matita/components/binaries/matex/kernel.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 F = Filename
  14 module P = Printf
  15 module S = String
  16
  17 module U = NUri
  18 module C = NCic
  19 module B = NCicSubstitution
  20 module D = NCicReduction
  21 module K = NCicTypeChecker
  22 module H = HLog
  23 module A = NCicLibrary
  24 module E = NCicEnvironment
  25 module R = NReference
  26
  27 module X = Ground
  28 module G = Options
  29
  30 (* internal functions *******************************************************)
  31
  32 let trusted _ = true
  33
  34 let no_log _ _ = ()
  35
  36 let mk_type_universe i =
  37    [`Type, U.uri_of_string (P.sprintf "cic:/matita/pts/Type%s.univ" i)]
  38
  39 (* interface functions ******************************************************)
  40
  41 let init () =
  42    A.init ();
  43    K.set_trust trusted;
  44    H.set_log_callback no_log;
  45    let u0 = mk_type_universe "0" in
  46    let u1 = mk_type_universe "1" in
  47    E.add_lt_constraint ~acyclic:true u0 u1
  48
  49 let fst_var = 1
  50
  51 let snd_var = 2
  52
  53 let appl ts = C.Appl ts
  54
  55 let prod s w t = C.Prod (s, w, t)
  56
  57 let lambda s w t = C.Lambda (s, w, t)
  58
  59 let letin s w v t = C.LetIn (s, w, v, t)
  60
  61 let case w u v ts = C.Match (w, u, v, ts)
  62
  63 let add_dec s w c = (s, C.Decl w) :: c
  64
  65 let add_def s w v c = (s, C.Def (v, w)) :: c
  66
  67 let rec shift t = function
  68    | []                     -> t
  69    | (s, C.Decl w) :: c     -> shift (lambda s w t) c
  70    | (s, C.Def (v, w)) :: c -> shift (letin s w v t) c
  71
  72 let rec is_atomic = function
  73    | C.Appl [t]   -> is_atomic t
  74    | C.Appl []
  75    | C.Meta _
  76    | C.Implicit _
  77    | C.Sort _
  78    | C.Rel _
  79    | C.Const _    -> true
  80    | C.Appl _
  81    | C.Prod _
  82    | C.Lambda _
  83    | C.LetIn _
  84    | C.Match _    -> false
  85
  86 let resolve_lref c i = fst (L.nth c (i - fst_var))
  87
  88 let lift d e t =
  89    B.lift G.status ~from:d e t
  90
  91 let lifts d e ts =
  92     L.rev_map (lift d e) (L.rev ts)
  93
  94 let whd c t =
  95    D.whd G.status ~delta:max_int ~subst:[] c t
  96
  97 let typeof c t =
  98    K.typeof G.status [] [] c t
  99
 100 let whd_typeof c t = whd c (typeof c t)
 101
 102 let not_prop1 c u = match whd_typeof c u with
 103    | C.Sort (C.Prop) -> false
 104    | _               -> true
 105
 106 let not_prop2 c t = not_prop1 c (typeof c t)
 107
 108 let does_not_occur i c t =
 109    K.does_not_occur G.status ~subst:[] c 0 i t
 110
 111 let segments_of_uri u =
 112    let s = U.string_of_uri u in
 113    let s = F.chop_extension s in
 114    let l = S.length s in
 115    let i = S.index s ':' in
 116    let s = S.sub s (i+2) (l-i-2) in
 117    X.segments_of_string [] (l-i-2) s
 118
 119 let names_of_reference ss = function
 120    | C.Constant (_, name, _, _, _), R.Decl      ->
 121       ss, name
 122    | C.Constant (_, name, _, _, _), R.Def _     ->
 123       ss, name
 124    | C.Inductive (_, _, us, _), R.Ind (_, i, _) ->
 125       let _, name, _, _ = L.nth us i in
 126       (name :: ss), name
 127    | C.Inductive (_, _, us, _), R.Con (i, j, _) ->
 128       let _, _, _, ts = L.nth us i in
 129       let _, name, _ = L.nth ts (pred j) in
 130       (name :: ss), name
 131    | C.Fixpoint (_, ts, _)    , R.Fix (i, _, _) ->
 132       let _, name, _, _, _ = L.nth ts i in
 133       (name :: ss), name
 134    | C.Fixpoint (_, ts, _)    , R.CoFix i       ->
 135       let _, name, _, _, _ = L.nth ts i in
 136       (name :: ss), name
 137    | _                                          ->
 138       failwith "name_of_reference"
 139
 140 let resolve_reference = function
 141    | R.Ref (u, r) ->
 142       let ss = segments_of_uri u in
 143       let _, _, _, _, obj = E.get_checked_obj G.status u in
 144       let ss, name = names_of_reference ss (obj, r) in
 145       X.rev_map_concat X.id "." "type" ss, name