matita/components/binaries/matex/alpha.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 module L = List
  13 module P = Printf
  14 module S = Scanf
  15 module N = String
  16 module H = Hashtbl
  17
  18 module U = NUri
  19 module C = NCic
  20 module R = NReference
  21 module E = NCicEnvironment
  22 module T = NCicTypeChecker
  23
  24 module X = Ground
  25 module G = Options
  26 module K = Kernel
  27
  28 type global = (string, int) H.t
  29
  30 type local = (string * int) list
  31
  32 type status = {
  33    g: global;    (* global context for alpha-conversion *)
  34    d: local;     (* local context for alpha-conversion *)
  35    c: C.context; (* local context for kernel calls *)
  36 }
  37
  38 (* internal functions *******************************************************)
  39
  40 let malformed s =
  41    X.error ("alpha: malformed term: " ^ s)
  42
  43 let ok s =
  44    X.log ("alpha: ok " ^ s)
  45
  46 let init () = {
  47    g = H.create 11; d = []; c = [];
  48 }
  49
  50 let rec trim r =
  51    let r1, r2 = S.sscanf r "%s@_%s" X.id2 in
  52    if r2 = "" then r1 else trim r1
  53
  54 let split s =
  55    let rec aux i l =
  56       let j = pred i in
  57       if j >=0 && s.[j] >= '0' && s.[j] <= '9' then aux j (succ l) else i, l
  58    in
  59    let i, l = aux (N.length s) 0 in
  60    let s1, s2 = N.sub s 0 i, N.sub s i l in
  61    let s1 = if s1 = "" then "_" else s1 in
  62    s1, if l = 0 then G.nan else int_of_string s2
  63
  64 let rec strip = function
  65    | C.Appl (t :: _)
  66    | C.Prod (_, _, t) -> strip t
  67    | t                -> t
  68
  69 let get_constant c t = match strip (K.whd c t) with
  70    | C.Sort (C.Prop)             ->
  71       P.sprintf "Prop"
  72    | C.Sort (C.Type [`Type, u])  ->
  73       P.sprintf "Type[%s]" (U.string_of_uri u)
  74    | C.Sort (C.Type [`CProp, u]) ->
  75       P.sprintf "CProp[%s]" (U.string_of_uri u)
  76    | C.Const (R.Ref (u, r))      ->
  77       let ss = K.segments_of_uri u in
  78       let _, _, _, _, obj = E.get_checked_obj G.status u in
  79       let ss, _ = K.name_of_reference ss (obj, r) in
  80       X.rev_map_concat X.id "." "type" ss
  81    | _                           -> ""
  82
  83 let read l s r =
  84    let rec aux = function
  85       | []              -> ""
  86       | (a, b, c) :: tl ->
  87          if s = a && (r = b || r = c) then c else aux tl
  88    in
  89    aux l
  90
  91 let type_check r c w =
  92    let s0 = get_constant c w in
  93    let r0 = read !G.alpha_type s0 r in
  94    if r0 <> "" then r0 else
  95    let s1 = get_constant c (K.typeof c w) in
  96    let r0 = read !G.alpha_sort s1 r in
  97    if r0 <> "" then r0 else begin
  98       if !G.log_alpha then
  99          X.log (P.sprintf "alpha: not found %s: type \"%s\" sort \"%s\"" r s0 s1);
 100       r
 101    end
 102
 103 let rec get r = function
 104    | []           -> r
 105    | (h, d) :: tl ->
 106       if fst r = h && snd r <= d then h, succ d else get r tl
 107
 108 let mk_name (s, i) =
 109    if i < 0 then s else P.sprintf "%s%u" s i
 110
 111 let local_alpha st s w t =
 112    if K.does_not_occur K.fst_var st.c t then G.dno_id, G.nan else
 113    let r, i = split (trim s) in
 114    get (type_check r st.c w, i) st.d
 115
 116 let global_apha st s =
 117 try
 118    let i = H.find st.g s in
 119    H.replace st.g s (succ i);
 120    P.sprintf "%s.%u" s i
 121 with Not_found ->
 122    H.add st.g s 0;
 123    s
 124
 125 let alpha st s w t =
 126    let r = local_alpha st s w t in
 127    let s = mk_name r in
 128    r, if G.is_global_id s then global_apha st s else s
 129
 130 let add_name r d = r :: d
 131
 132 let rec proc_term st t = match t with
 133    | C.Meta _
 134    | C.Implicit _
 135    | C.Sort _
 136    | C.Rel _
 137    | C.Const _             -> t
 138    | C.Appl ts             ->
 139       let tts = proc_terms st ts in
 140       K.appl tts
 141    | C.Match (w, u, v, ts) ->
 142       let uu = proc_term st u in
 143       let vv = proc_term st v in
 144       let tts = proc_terms st ts in
 145       K.case w uu vv tts
 146    | C.Prod (s, w, t)    ->
 147       let rr, ss = alpha st s w t in
 148       let ww = proc_term st w in
 149       let tt = proc_term {st with d=add_name rr st.d; c=K.add_dec ss w st.c} t in
 150       K.prod ss ww tt
 151    | C.Lambda (s, w, t)    ->
 152       let rr, ss = alpha st s w t in
 153       let ww = proc_term st w in
 154       let tt = proc_term {st with d=add_name rr st.d; c=K.add_dec ss w st.c} t in
 155       K.lambda ss ww tt
 156    | C.LetIn (s, w, v, t)  ->
 157       let rr, ss = alpha st s w t in
 158       let ww = proc_term st w in
 159       let vv = proc_term st v in
 160       let tt = proc_term {st with d=add_name rr st.d; c=K.add_def ss w v st.c} t in
 161       K.letin ss ww vv tt
 162
 163 and proc_terms st ts =
 164    let rtts = L.rev_map (proc_term st) ts in
 165    L.rev rtts
 166
 167 let proc_named_term s st t =
 168 try
 169    let tt = proc_term st t in
 170    if !G.test then begin
 171       let _ = K.typeof st.c tt in
 172       ok s
 173    end;
 174    tt
 175 with
 176    | T.TypeCheckerFailure s
 177    | T.AssertFailure s           -> malformed (Lazy.force s)
 178
 179 (* interface functions ******************************************************)
 180
 181 let process_top_term s t = proc_named_term s (init ()) t
 182