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