matita/components/ng_kernel/nCicUntrusted.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id$ *)
  13
  14 module C = NCic
  15 module Ref = NReference
  16
  17 let map_term_fold_a status g k f a = function
  18  | C.Meta _ -> assert false
  19  | C.Implicit _
  20  | C.Sort _
  21  | C.Const _
  22  | C.Rel _ as t -> a,t
  23  | C.Appl [] | C.Appl [_] -> assert false
  24  | C.Appl l as orig ->
  25     let fire_beta, upto =
  26       match l with C.Meta _ :: _ -> true, List.length l - 1 | _ -> false, 0
  27     in
  28     let a,l1 = HExtlib.sharing_map_acc (f k) a l in
  29     a, if l1 == l then orig else
  30        let t =
  31         match l1 with
  32          | C.Appl l :: tl -> C.Appl (l@tl)
  33          | _ -> C.Appl l1
  34        in
  35         if fire_beta then NCicReduction.head_beta_reduce status ~upto t
  36         else t
  37  | C.Prod (n,s,t) as orig ->
  38      let a,s1 = f k a s in let a,t1 = f (g (n,C.Decl s) k) a t in
  39      a, if t1 == t && s1 == s then orig else C.Prod (n,s1,t1)
  40  | C.Lambda (n,s,t) as orig ->
  41      let a,s1 = f k a s in let a,t1 = f (g (n,C.Decl s) k) a t in
  42      a, if t1 == t && s1 == s then orig else C.Lambda (n,s1,t1)
  43  | C.LetIn (n,ty,t,b) as orig ->
  44      let a,ty1 = f k a ty in let a,t1 = f k a t in
  45      let a,b1 = f (g (n,C.Def (t,ty)) k) a b in
  46      a, if ty1 == ty && t1 == t && b1 == b then orig else C.LetIn (n,ty1,t1,b1)
  47  | C.Match (r,oty,t,pl) as orig ->
  48      let a,oty1 = f k a oty in let a,t1 = f k a t in
  49      let a,pl1 = HExtlib.sharing_map_acc (f k) a pl in
  50      a, if oty1 == oty && t1 == t && pl1 == pl then orig
  51         else C.Match(r,oty1,t1,pl1)
  52 ;;
  53
  54 let metas_of_term status subst context term =
  55   let rec aux ctx acc = function
  56     | NCic.Rel i ->
  57          (match HExtlib.list_skip (i-1) ctx with
  58          | (_,NCic.Def (bo,_)) :: ctx -> aux ctx acc bo
  59          | _ -> acc)
  60     | NCic.Meta(i,l) ->
  61          (try
  62            let _,_,bo,_ = NCicUtils.lookup_subst i subst in
  63            let bo = NCicSubstitution.subst_meta status l bo in
  64            aux ctx acc bo
  65          with NCicUtils.Subst_not_found _ ->
  66             let shift, lc = l in
  67             let lc = NCicUtils.expand_local_context lc in
  68             let l = List.map (NCicSubstitution.lift status shift) lc in
  69             List.fold_left (aux ctx) (i::acc) l)
  70     | t -> NCicUtils.fold (fun e c -> e::c) ctx aux acc t
  71   in
  72     HExtlib.list_uniq (List.sort Pervasives.compare (aux context [] term))
  73 ;;
  74
  75 module NCicHash =
  76  Hashtbl.Make
  77   (struct
  78     type t = C.term
  79     let equal = (==)
  80     let hash = Hashtbl.hash_param 100 1000
  81    end)
  82 ;;
  83
  84 let mk_appl he args =
  85   if args = [] then he else
  86   match he with
  87   | NCic.Appl l -> NCic.Appl (l@args)
  88   | _ -> NCic.Appl (he::args)
  89 ;;
  90
  91 let map_obj_kind ?(skip_body=false) f =
  92  let do_bo f x = if skip_body then x else f x in
  93  function
  94     NCic.Constant (relev,name,bo,ty,attrs) ->
  95      NCic.Constant (relev,name,do_bo (HExtlib.map_option f) bo, f ty,attrs)
  96   | NCic.Fixpoint (ind,fl,attrs) ->
  97      let fl =
  98       List.map
  99        (function (relevance,name,recno,ty,bo) ->
 100           relevance,name,recno,f ty,do_bo f bo)
 101        fl
 102      in
 103       NCic.Fixpoint (ind,fl,attrs)
 104   | NCic.Inductive (is_ind,lno,itl,attrs) ->
 105       let itl =
 106         List.map
 107          (fun (relevance,name,ty,cl) ->
 108            let cl =
 109              List.map (fun (relevance, name, ty) ->
 110                 relevance, name, f ty)
 111              cl
 112            in
 113            relevance, name, f ty, cl)
 114          itl
 115       in
 116       NCic.Inductive (is_ind,lno,itl,attrs)
 117 ;;
 118
 119 exception Occurr;;
 120
 121 let clean_or_fix_dependent_abstrations status ctx t =
 122   let occurrs_1 t =
 123     let rec aux n _ = function
 124       | NCic.Meta _ -> ()
 125       | NCic.Rel i when i = n + 1 -> raise Occurr
 126       | t -> NCicUtils.fold (fun _ k -> k + 1) n aux () t
 127     in
 128     try aux 0 () t; false
 129     with Occurr -> true
 130   in
 131   let fresh ctx name =
 132     if not (List.mem name ctx) then name
 133     else
 134      let rec aux i =
 135        let attempt = name ^ string_of_int i in
 136        if List.mem attempt ctx then aux (i+1)
 137        else attempt
 138      in
 139       aux 0
 140   in
 141   let rec aux ctx = function
 142   | NCic.Meta _ as t -> t
 143   | NCic.Prod (name,s,t) when name.[0] = '#' && occurrs_1 t ->
 144       let name = fresh ctx (String.sub name 1 (String.length name-1)) in
 145       NCic.Prod (name,aux ctx s, aux (name::ctx) t)
 146   | NCic.Prod (name,s,t) when name.[0] = '#' && not (occurrs_1 t) ->
 147       NCic.Prod ("_",aux ctx s,aux ("_"::ctx) t)
 148   | NCic.Prod ("_",s,t) -> NCic.Prod("_",aux ctx s,aux ("_"::ctx) t)
 149   | NCic.Prod (name,s,t) when name.[0] <> '_' && not (occurrs_1 t) ->
 150       let name = fresh ctx ("_"^name) in
 151       NCic.Prod (name, aux ctx s, aux (name::ctx) t)
 152   | NCic.Prod (name,s,t) when List.mem name ctx ->
 153       let name = fresh ctx name in
 154       NCic.Prod (name, aux ctx s, aux (name::ctx) t)
 155   | NCic.Lambda (name,s,t) when List.mem name ctx ->
 156       let name = fresh ctx name in
 157       NCic.Lambda (name, aux ctx s, aux (name::ctx) t)
 158   | t -> NCicUtils.map status (fun (e,_) ctx -> e::ctx) ctx aux t
 159   in
 160     aux (List.map fst ctx) t
 161 ;;
 162
 163 let rec fire_projection_redex status on_args = function
 164   | C.Meta _ as t -> t
 165   | C.Appl(C.Const(Ref.Ref(_,Ref.Fix(fno,rno,_)) as r)::args as ol)as ot->
 166       let l= if on_args then List.map (fire_projection_redex status true) ol else ol in
 167       let t = if l == ol then ot else C.Appl l in
 168       let ifl,(_,_,pragma),_ = NCicEnvironment.get_checked_fixes_or_cofixes status r in
 169       let conclude () =
 170         if on_args then
 171           let l' = HExtlib.sharing_map (fire_projection_redex status true) l in
 172           if l == l' then t else C.Appl l'
 173         else
 174           t (* ot is the same *)
 175       in
 176       if pragma <> `Projection || List.length args <= rno then conclude ()
 177       else
 178         (match List.nth l (rno+1) with
 179         | C.Appl (C.Const(Ref.Ref(_,Ref.Con _))::_) ->
 180             let _, _, _, _, fbody = List.nth ifl fno in (* fbody is closed! *)
 181             let t = C.Appl (fbody::List.tl l) in
 182             (match NCicReduction.head_beta_reduce status ~delta:max_int t with
 183              | C.Match (_,_, C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))
 184                 ::kargs),[pat])->
 185                   let _,kargs = HExtlib.split_nth leftno kargs in
 186                    fire_projection_redex status false
 187                     (NCicReduction.head_beta_reduce status
 188                       ~delta:max_int (C.Appl (pat :: kargs)))
 189             | C.Appl(C.Match(_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))
 190                ::kargs),[pat]) :: args) ->
 191                   let _,kargs = HExtlib.split_nth leftno kargs in
 192                    fire_projection_redex status false
 193                     (NCicReduction.head_beta_reduce status
 194                       ~delta:max_int (C.Appl (pat :: kargs @ args)))
 195             | _ -> conclude ())
 196         | _ -> conclude ())
 197   | t when on_args ->
 198      NCicUtils.map status (fun _ x -> x) true (fire_projection_redex status) t
 199   | t -> t
 200 ;;
 201
 202 let apply_subst status ?(fix_projections=false) subst context t =
 203  let rec apply_subst subst () =
 204  function
 205     NCic.Meta (i,lc) ->
 206      (try
 207        let _,_,t,_ = NCicUtils.lookup_subst i subst in
 208        let t = NCicSubstitution.subst_meta status lc t in
 209         apply_subst subst () t
 210       with
 211        NCicUtils.Subst_not_found j when j = i ->
 212         match lc with
 213            _,NCic.Irl _ -> NCic.Meta (i,lc)
 214          | n,NCic.Ctx l ->
 215             NCic.Meta
 216              (i,(0,NCic.Ctx
 217                  (List.map (fun t ->
 218                    apply_subst subst () (NCicSubstitution.lift status n t)) l))))
 219   | t -> NCicUtils.map status (fun _ () -> ()) () (apply_subst subst) t
 220  in
 221  (if fix_projections then fire_projection_redex status true else fun x -> x)
 222     (clean_or_fix_dependent_abstrations status context (apply_subst subst () t))
 223 ;;
 224
 225 let apply_subst_context status ~fix_projections subst context =
 226   let apply_subst = apply_subst status ~fix_projections in
 227   let rec aux c = function
 228     | [] -> []
 229     | (name,NCic.Decl t as e) :: tl ->
 230         (name, NCic.Decl (apply_subst subst c t)) :: aux (e::c) tl
 231     | (name,NCic.Def (t1,t2) as e) :: tl ->
 232         (name, NCic.Def (apply_subst subst c t1,apply_subst subst c t2)) ::
 233           aux (e::c) tl
 234   in
 235     List.rev (aux [] (List.rev context))
 236 ;;
 237
 238 let rec apply_subst_metasenv status subst = function
 239   | [] -> []
 240   | (i,_) :: _ when List.mem_assoc i subst -> assert false
 241   | (i,(name,ctx,ty)) :: tl ->
 242       (i,(name,apply_subst_context status ~fix_projections:true subst ctx,
 243                apply_subst status ~fix_projections:true subst ctx ty)) ::
 244          apply_subst_metasenv status subst tl
 245 ;;
 246
 247 (* hide optional arg *)
 248 let apply_subst status s c t = apply_subst status s c t;;
 249
 250
 251 type meta_kind = [ `IsSort | `IsType | `IsTerm ]
 252
 253 let is_kind x = x = `IsSort || x = `IsType || x = `IsTerm ;;
 254
 255 let kind_of_meta l =
 256   try
 257     (match List.find is_kind l with
 258     | `IsSort | `IsType | `IsTerm as x -> x
 259     | _ -> assert false)
 260   with
 261    Not_found -> assert false
 262 ;;
 263
 264 let rec replace_in_metasenv i f = function
 265   | [] -> assert false
 266   | (j,e)::tl when j=i -> (i,f e) :: tl
 267   | x::tl -> x :: replace_in_metasenv i f tl
 268 ;;
 269
 270 let rec replace_in_subst i f = function
 271   | [] -> assert false
 272   | (j,e)::tl when j=i -> (i,f e) :: tl
 273   | x::tl -> x :: replace_in_subst i f tl
 274 ;;
 275
 276 let set_kind newkind attrs =
 277   newkind :: List.filter (fun x -> not (is_kind x)) attrs
 278 ;;
 279
 280 let max_kind k1 k2 =
 281   match k1, k2 with
 282   | `IsSort, _ | _, `IsSort -> `IsSort
 283   | `IsType, _ | _, `IsType -> `IsType
 284   | _ -> `IsTerm
 285 ;;
 286
 287 module OT =
 288   struct
 289     type t = int * NCic.conjecture
 290     let compare (i,_) (j,_) = Pervasives.compare i j
 291   end
 292
 293 module MS = HTopoSort.Make(OT)
 294 let relations_of_menv status subst m c =
 295   let i, (_, ctx, ty) = c in
 296   let m = List.filter (fun (j,_) -> j <> i) m in
 297   let m_ty = metas_of_term status subst ctx ty in
 298   let m_ctx =
 299    snd
 300     (List.fold_right
 301      (fun i (ctx,res) ->
 302       (i::ctx),
 303       (match i with
 304        | _,NCic.Decl ty -> metas_of_term status subst ctx ty
 305        | _,NCic.Def (t,ty) ->
 306          metas_of_term status subst ctx ty @ metas_of_term status subst ctx t) @ res)
 307     ctx ([],[]))
 308   in
 309   let metas = HExtlib.list_uniq (List.sort compare (m_ty @ m_ctx)) in
 310   List.filter (fun (i,_) -> List.exists ((=) i) metas) m
 311 ;;
 312
 313 let sort_metasenv status subst (m : NCic.metasenv) =
 314   (MS.topological_sort m (relations_of_menv status subst m) : NCic.metasenv)
 315 ;;
 316
 317 let count_occurrences status ~subst n t =
 318   let occurrences = ref 0 in
 319   let rec aux k _ = function
 320     | C.Rel m when m = n+k -> incr occurrences
 321     | C.Rel _m -> ()
 322     | C.Implicit _ -> ()
 323     | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) ()
 324     | C.Meta (mno,(s,l)) ->
 325          (try
 326             (* possible optimization here: try does_not_occur on l and
 327                perform substitution only if DoesOccur is raised *)
 328             let _,_,term,_ = NCicUtils.lookup_subst mno subst in
 329             aux (k-s) () (NCicSubstitution.subst_meta status (0,l) term)
 330           with NCicUtils.Subst_not_found _ -> () (*match l with
 331           | C.Irl len -> if not (n+k >= s+len || s > nn+k) then raise DoesOccur
 332           | C.Ctx lc -> List.iter (aux (k-s) ()) lc*))
 333     | t -> NCicUtils.fold (fun _ k -> k + 1) k aux () t
 334   in
 335    aux 0 () t;
 336    !occurrences
 337 ;;
 338
 339 exception Found_variable
 340
 341 let looks_closed t =
 342   let rec aux k _ = function
 343     | C.Rel m when k < m -> raise Found_variable
 344     | C.Rel _m -> ()
 345     | C.Implicit _ -> ()
 346     | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) ()
 347     | C.Meta _ -> raise Found_variable
 348     | t -> NCicUtils.fold (fun _ k -> k + 1) k aux () t
 349   in
 350   try aux 0 () t; true with Found_variable -> false
 351 ;;