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 ->
  91         let (metasenv', idx) = mk_implicit metasenv context in
  92         let irl = identity_relocation_list_for_metavariable context in
  93         metasenv', Cic.Meta (idx, irl)
  94     | Cic.Cast (te, ty) ->
  95         let metasenv', ty' = aux metasenv context ty in
  96         let metasenv'', te' = aux metasenv' context te in
  97         metasenv'', Cic.Cast (te', ty')
  98     | Cic.Prod (name, s, t) ->
  99         let metasenv', s' = aux metasenv context s in
 100         let metasenv'', t' =
 101           aux metasenv' (Some (name, Cic.Decl s') :: context) t
 102         in
 103         metasenv'', Cic.Prod (name, s', t')
 104     | Cic.Lambda (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.Lambda (name, s', t')
 110     | Cic.LetIn (name, s, t) ->
 111         let metasenv', s' = aux metasenv context s in
 112         let metasenv'', t' =
 113           aux metasenv' (Some (name, Cic.Def (s', None)) :: context) t
 114         in
 115         metasenv'', Cic.LetIn (name, s', t')
 116     | Cic.Appl l when List.length l > 1 ->
 117         let metasenv', l' =
 118           List.fold_right
 119             (fun term (metasenv, terms) ->
 120               let new_metasenv, term = aux metasenv context term in
 121               new_metasenv, term :: terms)
 122             l (metasenv, [])
 123         in
 124         metasenv', Cic.Appl l'
 125     | Cic.Appl _ -> assert false
 126     | Cic.MutCase (uri, i, outtype, term, patterns) ->
 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             (outtype :: term :: patterns) (metasenv, [])
 133         in
 134         let outtype', term', patterns' =
 135           match l' with
 136           | outtype' :: term' :: patterns' -> outtype', term', patterns'
 137           | _ -> assert false
 138         in
 139         metasenv', Cic.MutCase (uri, i, outtype', term', patterns')
 140     | Cic.Fix (i, funs) ->
 141         let metasenv', types =
 142           List.fold_right
 143             (fun (name, _, typ, _) (metasenv, types) ->
 144               let new_metasenv, new_type = aux metasenv context typ in
 145 prerr_endline ("UH? " ^ CicPp.ppterm typ ^ " ==> " ^ CicPp.ppterm new_type) ;
 146               (new_metasenv, (name, new_type) :: types))
 147             funs (metasenv, [])
 148         in
 149         let context' =
 150           (List.rev_map
 151             (fun (name, t) -> Some (Cic.Name name, Cic.Decl t))
 152             types)
 153           @ context
 154         in
 155         let metasenv'', bodies =
 156           List.fold_right
 157             (fun (_, _, _, body) (metasenv, bodies) ->
 158               let new_metasenv, new_body = aux metasenv context' body in
 159               (new_metasenv, new_body :: bodies))
 160             funs (metasenv', [])
 161         in
 162         let rec combine = function
 163           | ((name, index, _, _) :: funs_tl),
 164             ((_, typ) :: typ_tl),
 165             (body :: body_tl) ->
 166               (name, index, typ, body) :: combine (funs_tl, typ_tl, body_tl)
 167           | [], [], [] -> []
 168           | _ -> assert false
 169         in
 170         let funs' = combine (funs, types, bodies) in
 171         metasenv'', Cic.Fix (i, funs')
 172     | Cic.CoFix (i, funs) ->
 173         let metasenv', types =
 174           List.fold_right
 175             (fun (name, typ, _) (metasenv, types) ->
 176               let new_metasenv, new_type = aux metasenv context typ in
 177               (new_metasenv, (name, new_type) :: types))
 178             funs (metasenv, [])
 179         in
 180         let context' =
 181           (List.rev_map
 182             (fun (name, t) -> Some (Cic.Name name, Cic.Decl t))
 183             types)
 184           @ context
 185         in
 186         let metasenv'', bodies =
 187           List.fold_right
 188             (fun (_, _, body) (metasenv, bodies) ->
 189               let new_metasenv, new_body = aux metasenv context' body in
 190               (new_metasenv, new_body :: bodies))
 191             funs (metasenv', [])
 192         in
 193         let rec combine = function
 194           | ((name, _, _) :: funs_tl),
 195             ((_, typ) :: typ_tl),
 196             (body :: body_tl) ->
 197               (name, typ, body) :: combine (funs_tl, typ_tl, body_tl)
 198           | [], [], [] -> []
 199           | _ -> assert false
 200         in
 201         let funs' = combine (funs, types, bodies) in
 202         metasenv'', Cic.CoFix (i, funs')
 203   and do_subst metasenv context subst =
 204     List.fold_right
 205       (fun (uri, term) (metasenv, substs) ->
 206         let metasenv', term' = aux metasenv context term in
 207         (metasenv', (uri, term') :: substs))
 208       subst (metasenv, [])
 209   and do_local_context metasenv context local_context =
 210     List.fold_right
 211       (fun term (metasenv, local_context) ->
 212         let metasenv', term' =
 213           match term with
 214           | None -> metasenv, None
 215           | Some term ->
 216               let metasenv', term' = aux metasenv context term in
 217               metasenv', Some term'
 218         in
 219         metasenv', term' :: local_context)
 220       local_context (metasenv, [])
 221   in
 222   aux metasenv context term
 223