helm/software/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 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 =
  29       (* sharing fold? *)
  30       List.fold_right
  31         (fun t (a,l) -> let a,t = f k a t in a, t :: l)
  32         l (a,[])
  33     in
  34     a, if l1 == l then orig else
  35        let t =
  36         match l1 with
  37          | C.Appl l :: tl -> C.Appl (l@tl)
  38          | _ -> C.Appl l1
  39        in
  40         if fire_beta then NCicReduction.head_beta_reduce ~upto t
  41         else t
  42  | C.Prod (n,s,t) as orig ->
  43      let a,s1 = f k a s in let a,t1 = f (g (n,C.Decl s) k) a t in
  44      a, if t1 == t && s1 == s then orig else C.Prod (n,s1,t1)
  45  | C.Lambda (n,s,t) as orig ->
  46      let a,s1 = f k a s in let a,t1 = f (g (n,C.Decl s) k) a t in
  47      a, if t1 == t && s1 == s then orig else C.Lambda (n,s1,t1)
  48  | C.LetIn (n,ty,t,b) as orig ->
  49      let a,ty1 = f k a ty in let a,t1 = f k a t in
  50      let a,b1 = f (g (n,C.Def (t,ty)) k) a b in
  51      a, if ty1 == ty && t1 == t && b1 == b then orig else C.LetIn (n,ty1,t1,b1)
  52  | C.Match (r,oty,t,pl) as orig ->
  53      let a,oty1 = f k a oty in let a,t1 = f k a t in
  54      let a,pl1 =
  55        (* sharing fold? *)
  56        List.fold_right (fun t (a,l) -> let a,t = f k a t in a,t::l) pl (a,[])
  57      in
  58      a, if oty1 == oty && t1 == t && pl1 == pl then orig
  59         else C.Match(r,oty1,t1,pl1)
  60 ;;
  61
  62 let metas_of_term subst context term =
  63   let rec aux ctx acc = function
  64     | NCic.Rel i ->
  65          (match HExtlib.list_skip (i-1) ctx with
  66          | (_,NCic.Def (bo,_)) :: ctx -> aux ctx acc bo
  67          | _ -> acc)
  68     | NCic.Meta(i,l) ->
  69          (try
  70            let _,_,bo,_ = NCicUtils.lookup_subst i subst in
  71            let bo = NCicSubstitution.subst_meta l bo in
  72            aux ctx acc bo
  73          with NCicUtils.Subst_not_found _ ->
  74             let shift, lc = l in
  75             let lc = NCicUtils.expand_local_context lc in
  76             let l = List.map (NCicSubstitution.lift shift) lc in
  77             List.fold_left (aux ctx) (i::acc) l)
  78     | t -> NCicUtils.fold (fun e c -> e::c) ctx aux acc t
  79   in
  80     HExtlib.list_uniq (List.sort Pervasives.compare (aux context [] term))
  81 ;;
  82
  83 module NCicHash =
  84  Hashtbl.Make
  85   (struct
  86     type t = C.term
  87     let equal = (==)
  88     let hash = Hashtbl.hash_param 100 1000
  89    end)
  90 ;;
  91
  92 let mk_appl he args =
  93   if args = [] then he else
  94   match he with
  95   | NCic.Appl l -> NCic.Appl (l@args)
  96   | _ -> NCic.Appl (he::args)
  97 ;;
  98
  99 let map_obj_kind ?(skip_body=false) f =
 100  let do_bo f x = if skip_body then x else f x in
 101  function
 102     NCic.Constant (relev,name,bo,ty,attrs) ->
 103      NCic.Constant (relev,name,do_bo (HExtlib.map_option f) bo, f ty,attrs)
 104   | NCic.Fixpoint (ind,fl,attrs) ->
 105      let fl =
 106       List.map
 107        (function (relevance,name,recno,ty,bo) ->
 108           relevance,name,recno,f ty,do_bo f bo)
 109        fl
 110      in
 111       NCic.Fixpoint (ind,fl,attrs)
 112   | NCic.Inductive (is_ind,lno,itl,attrs) ->
 113       let itl =
 114         List.map
 115          (fun (relevance,name,ty,cl) ->
 116            let cl =
 117              List.map (fun (relevance, name, ty) ->
 118                 relevance, name, f ty)
 119              cl
 120            in
 121            relevance, name, f ty, cl)
 122          itl
 123       in
 124       NCic.Inductive (is_ind,lno,itl,attrs)
 125 ;;
 126
 127 exception Occurr;;
 128
 129 let clean_or_fix_dependent_abstrations ctx t =
 130   let occurrs_1 t =
 131     let rec aux n _ = function
 132       | NCic.Meta _ -> ()
 133       | NCic.Rel i when i = n + 1 -> raise Occurr
 134       | t -> NCicUtils.fold (fun _ k -> k + 1) n aux () t
 135     in
 136     try aux 0 () t; false
 137     with Occurr -> true
 138   in
 139   let fresh ctx name =
 140     if not (List.mem name ctx) then name
 141     else
 142      let rec aux i =
 143        let attempt = name ^ string_of_int i in
 144        if List.mem attempt ctx then aux (i+1)
 145        else attempt
 146      in
 147       aux 0
 148   in
 149   let rec aux ctx = function
 150   | NCic.Meta _ as t -> t
 151   | NCic.Prod (name,s,t) when name.[0] = '#' && occurrs_1 t ->
 152       let name = fresh ctx (String.sub name 1 (String.length name-1)) in
 153       NCic.Prod (name,aux ctx s, aux (name::ctx) t)
 154   | NCic.Prod (name,s,t) when name.[0] = '#' && not (occurrs_1 t) ->
 155       NCic.Prod ("_",aux ctx s,aux ("_"::ctx) t)
 156   | NCic.Prod ("_",s,t) -> NCic.Prod("_",aux ctx s,aux ("_"::ctx) t)
 157   | NCic.Prod (name,s,t) when name.[0] <> '_' && not (occurrs_1 t) ->
 158       let name = fresh ctx ("_"^name) in
 159       NCic.Prod (name, aux ctx s, aux (name::ctx) t)
 160   | NCic.Prod (name,s,t) when List.mem name ctx ->
 161       let name = fresh ctx name in
 162       NCic.Prod (name, aux ctx s, aux (name::ctx) t)
 163   | NCic.Lambda (name,s,t) when List.mem name ctx ->
 164       let name = fresh ctx name in
 165       NCic.Lambda (name, aux ctx s, aux (name::ctx) t)
 166   | t -> NCicUtils.map (fun (e,_) ctx -> e::ctx) ctx aux t
 167   in
 168     aux (List.map fst ctx) t
 169 ;;
 170
 171 let apply_subst subst context t =
 172  let rec apply_subst subst () =
 173  function
 174     NCic.Meta (i,lc) ->
 175      (try
 176        let _,_,t,_ = NCicUtils.lookup_subst i subst in
 177        let t = NCicSubstitution.subst_meta lc t in
 178         apply_subst subst () t
 179       with
 180        Not_found ->
 181         match lc with
 182            _,NCic.Irl _ -> NCic.Meta (i,lc)
 183          | n,NCic.Ctx l ->
 184             NCic.Meta
 185              (i,(0,NCic.Ctx
 186                  (List.map (fun t ->
 187                    apply_subst subst () (NCicSubstitution.lift n t)) l))))
 188   | t -> NCicUtils.map (fun _ () -> ()) () (apply_subst subst) t
 189  in
 190   clean_or_fix_dependent_abstrations context (apply_subst subst () t)
 191 ;;
 192
 193 let apply_subst_context subst context =
 194   let rec aux c = function
 195     | [] -> []
 196     | (name,NCic.Decl t as e) :: tl ->
 197         (name, NCic.Decl (apply_subst subst c t)) :: aux (e::c) tl
 198     | (name,NCic.Def (t1,t2) as e) :: tl ->
 199         (name, NCic.Def (apply_subst subst c t1,apply_subst subst c t2)) ::
 200           aux (e::c) tl
 201   in
 202     List.rev (aux [] (List.rev context))
 203 ;;
 204
 205 let rec apply_subst_metasenv subst = function
 206   | [] -> []
 207   | (i,_) :: _ when List.mem_assoc i subst -> assert false
 208   | (i,(name,ctx,ty)) :: tl ->
 209       (i,(name,apply_subst_context subst ctx,apply_subst subst ctx ty)) ::
 210          apply_subst_metasenv subst tl
 211 ;;