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 u0 u1
  48
  49 let fst_var = 1
  50
  51 let snd_var = 2
  52
  53 let lambda s w t = C.Lambda (s, w, t)
  54
  55 let letin s w v t = C.LetIn (s, w, v, t)
  56
  57 let case w u v ts = C.Match (w, u, v, ts)
  58
  59 let add_dec s w c = (s, C.Decl w) :: c
  60
  61 let add_def s w v c = (s, C.Def (v, w)) :: c
  62
  63 let rec shift t = function
  64    | []                     -> t
  65    | (s, C.Decl w) :: c     -> shift (lambda s w t) c
  66    | (s, C.Def (v, w)) :: c -> shift (letin s w v t) c
  67
  68 let rec is_atomic = function
  69    | C.Appl [t]   -> is_atomic t
  70    | C.Appl []
  71    | C.Meta _
  72    | C.Implicit _
  73    | C.Sort _
  74    | C.Rel _
  75    | C.Const _    -> true
  76    | C.Appl _
  77    | C.Prod _
  78    | C.Lambda _
  79    | C.LetIn _
  80    | C.Match _    -> false
  81
  82 let resolve_lref c i = fst (L.nth c (i - fst_var))
  83
  84 let lift d e t =
  85    B.lift G.status ~from:d e t
  86
  87 let lifts d e ts =
  88     L.rev_map (lift d e) (L.rev ts)
  89
  90 let whd c t =
  91    D.whd G.status ~delta:max_int ~subst:[] c t
  92
  93 let typeof c t =
  94    K.typeof G.status [] [] c t
  95
  96 let segments_of_uri u =
  97    let s = U.string_of_uri u in
  98    let s = F.chop_extension s in
  99    let l = S.length s in
 100    let i = S.index s ':' in
 101    let s = S.sub s (i+2) (l-i-2) in
 102    X.segments_of_string [] (l-i-2) s
 103
 104 let name_of_reference ss = function
 105    | C.Constant (_, name, _, _, _), R.Decl      ->
 106       ss, name
 107    | C.Constant (_, name, _, _, _), R.Def _     ->
 108       ss, name
 109    | C.Inductive (_, _, us, _), R.Ind (_, i, _) ->
 110       let _, name, _, _ = L.nth us i in
 111       (name :: ss), name
 112    | C.Inductive (_, _, us, _), R.Con (i, j, _) ->
 113       let _, _, _, ts = L.nth us i in
 114       let _, name, _ = L.nth ts (pred j) in
 115       (name :: ss), name
 116    | C.Fixpoint (_, ts, _)    , R.Fix (i, _, _) ->
 117       let _, name, _, _, _ = L.nth ts i in
 118       (name :: ss), name
 119    | C.Fixpoint (_, ts, _)    , R.CoFix i       ->
 120       let _, name, _, _, _ = L.nth ts i in
 121       (name :: ss), name
 122    | _                                          ->
 123       failwith "name_of_reference"