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 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 (1,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 mk_implicit' metasenv context =
  37   let (metasenv, index) = mk_implicit metasenv context in
  38   (metasenv, index - 1, index)
  39
  40 let mk_implicit_type metasenv context =
  41   let newmeta = new_meta metasenv in
  42   let irl = identity_relocation_list_for_metavariable context in
  43   ([ newmeta, context, Cic.Sort Cic.Type ;
  44     newmeta + 1, context, Cic.Meta (newmeta, irl) ] @metasenv,
  45    newmeta + 1)
  46
  47 let expand_implicits metasenv context term =
  48   let rec aux metasenv context = function
  49     | (Cic.Rel _) as t -> metasenv, t
  50     | (Cic.Sort _) as t -> metasenv, t
  51     | Cic.Const (uri, subst) ->
  52         let metasenv', subst' = do_subst metasenv context subst in
  53         metasenv', Cic.Const (uri, subst')
  54     | Cic.Var (uri, subst) ->
  55         let metasenv', subst' = do_subst metasenv context subst in
  56         metasenv', Cic.Var (uri, subst')
  57     | Cic.MutInd (uri, i, subst) ->
  58         let metasenv', subst' = do_subst metasenv context subst in
  59         metasenv', Cic.MutInd (uri, i, subst')
  60     | Cic.MutConstruct (uri, i, j, subst) ->
  61         let metasenv', subst' = do_subst metasenv context subst in
  62         metasenv', Cic.MutConstruct (uri, i, j, subst')
  63     | Cic.Meta (n,l) ->
  64         let metasenv', l' = do_local_context metasenv context l in
  65         metasenv', Cic.Meta (n, l')
  66     | Cic.Implicit ->
  67         let (metasenv', type_index, _) = mk_implicit' metasenv context in
  68         let irl = identity_relocation_list_for_metavariable context in
  69         metasenv', Cic.Meta (type_index, irl)
  70     | Cic.Cast (te, ty) ->
  71         let metasenv', ty' = aux metasenv context ty in
  72         let metasenv'', te' = aux metasenv' context te in
  73         metasenv'', Cic.Cast (te', ty')
  74     | Cic.Prod (name, s, t) ->
  75         let metasenv', s' = aux metasenv context s in
  76         let metasenv'', t' =
  77           aux metasenv' (Some (name, Cic.Decl s') :: context) t
  78         in
  79         metasenv'', Cic.Prod (name, s', t')
  80     | Cic.Lambda (name, s, t) ->
  81         let metasenv', s' = aux metasenv context s in
  82         let metasenv'', t' =
  83           aux metasenv' (Some (name, Cic.Decl s') :: context) t
  84         in
  85         metasenv'', Cic.Lambda (name, s', t')
  86     | Cic.LetIn (name, s, t) ->
  87         let metasenv', s' = aux metasenv context s in
  88         let metasenv'', t' =
  89           aux metasenv' (Some (name, Cic.Def (s', None)) :: context) t
  90         in
  91         metasenv'', Cic.LetIn (name, s', t')
  92     | Cic.Appl l when List.length l > 1 ->
  93         let metasenv', l' =
  94           List.fold_right
  95             (fun term (metasenv, terms) ->
  96               let new_metasenv, term = aux metasenv context term in
  97               new_metasenv, term :: terms)
  98             l (metasenv, [])
  99         in
 100         metasenv', Cic.Appl l'
 101     | Cic.Appl _ -> assert false
 102     | Cic.MutCase (uri, i, outtype, term, patterns) ->
 103         let metasenv', l' =
 104           List.fold_right
 105             (fun term (metasenv, terms) ->
 106               let new_metasenv, term = aux metasenv context term in
 107               new_metasenv, term :: terms)
 108             (outtype :: term :: patterns) (metasenv, [])
 109         in
 110         let outtype', term', patterns' =
 111           match l' with
 112           | outtype' :: term' :: patterns' -> outtype', term', patterns'
 113           | _ -> assert false
 114         in
 115         metasenv', Cic.MutCase (uri, i, outtype', term', patterns')
 116     | Cic.Fix (i, funs) ->
 117         let metasenv', types =
 118           List.fold_right
 119             (fun (name, _, typ, _) (metasenv, types) ->
 120               let new_metasenv, new_type = aux metasenv context typ in
 121               (new_metasenv, (name, new_type) :: types))
 122             funs (metasenv, [])
 123         in
 124         let context' =
 125           (List.rev_map
 126             (fun (name, t) -> Some (Cic.Name name, Cic.Decl t))
 127             types)
 128           @ context
 129         in
 130         let metasenv'', bodies =
 131           List.fold_right
 132             (fun (_, _, _, body) (metasenv, bodies) ->
 133               let new_metasenv, new_body = aux metasenv context' body in
 134               (new_metasenv, new_body :: bodies))
 135             funs (metasenv', [])
 136         in
 137         let rec combine = function
 138           | ((name, index, _, _) :: funs_tl),
 139             ((_, typ) :: typ_tl),
 140             (body :: body_tl) ->
 141               (name, index, typ, term) :: combine (funs_tl, typ_tl, body_tl)
 142           | [], [], [] -> []
 143           | _ -> assert false
 144         in
 145         let funs' = combine (funs, types, bodies) in
 146         metasenv'', Cic.Fix (i, funs')
 147     | Cic.CoFix (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, _, _) :: funs_tl),
 170             ((_, typ) :: typ_tl),
 171             (body :: body_tl) ->
 172               (name, typ, term) :: combine (funs_tl, typ_tl, body_tl)
 173           | [], [], [] -> []
 174           | _ -> assert false
 175         in
 176         let funs' = combine (funs, types, bodies) in
 177         metasenv'', Cic.CoFix (i, funs')
 178   and do_subst metasenv context subst =
 179     List.fold_right
 180       (fun (uri, term) (metasenv, substs) ->
 181         let metasenv', term' = aux metasenv context term in
 182         (metasenv', (uri, term') :: substs))
 183       subst (metasenv, [])
 184   and do_local_context metasenv context local_context =
 185     List.fold_right
 186       (fun term (metasenv, local_context) ->
 187         let metasenv', term' =
 188           match term with
 189           | None -> metasenv, None
 190           | Some term ->
 191               let metasenv', term' = aux metasenv context term in
 192               metasenv', Some term'
 193         in
 194         metasenv', term' :: local_context)
 195       local_context (metasenv, [])
 196   in
 197   aux metasenv context term
 198