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 (* first variable *)
  50
  51 let snd_var = 2 (* second variable *)
  52
  53 let fst_con = 1 (* first constructor *)
  54
  55 let appl ts = C.Appl ts
  56
  57 let prod s w t = C.Prod (s, w, t)
  58
  59 let lambda s w t = C.Lambda (s, w, t)
  60
  61 let letin s w v t = C.LetIn (s, w, v, t)
  62
  63 let case w u v ts = C.Match (w, u, v, ts)
  64
  65 let add_dec s w c = (s, C.Decl w) :: c
  66
  67 let add_def s w v c = (s, C.Def (v, w)) :: c
  68
  69 let rec shift t = function
  70    | []                     -> t
  71    | (s, C.Decl w) :: c     -> shift (lambda s w t) c
  72    | (s, C.Def (v, w)) :: c -> shift (letin s w v t) c
  73
  74 let rec is_atomic = function
  75    | C.Appl [t]   -> is_atomic t
  76    | C.Appl []
  77    | C.Meta _
  78    | C.Implicit _
  79    | C.Sort _
  80    | C.Rel _
  81    | C.Const _    -> true
  82    | C.Appl _
  83    | C.Prod _
  84    | C.Lambda _
  85    | C.LetIn _
  86    | C.Match _    -> false
  87
  88 let resolve_lref c i = fst (L.nth c (i - fst_var))
  89
  90 let lift d e t =
  91    B.lift G.status ~from:d e t
  92
  93 let lifts d e ts =
  94     L.rev_map (lift d e) (L.rev ts)
  95
  96 let whd c t =
  97    D.whd G.status ~delta:max_int ~subst:[] c t
  98
  99 let typeof c t =
 100    K.typeof G.status [] [] c t
 101
 102 let whd_typeof c t = whd c (typeof c t)
 103
 104 let not_prop1 c u = match whd_typeof c u with
 105    | C.Sort (C.Prop) -> false
 106    | _               -> true
 107
 108 let not_prop2 c t = not_prop1 c (typeof c t)
 109
 110 let does_not_occur i c t =
 111    K.does_not_occur G.status ~subst:[] c 0 i t
 112
 113 let segments_of_uri u =
 114    let s = U.string_of_uri u in
 115    let s = F.chop_extension s in
 116    let l = S.length s in
 117    let i = S.index s ':' in
 118    let s = S.sub s (i+2) (l-i-2) in
 119    X.segments_of_string [] (l-i-2) s
 120
 121 let names_of_reference ss = function
 122    | C.Constant (_, name, _, _, _), R.Decl      ->
 123       ss, name
 124    | C.Constant (_, name, _, _, _), R.Def _     ->
 125       ss, name
 126    | C.Inductive (_, _, us, _), R.Ind (_, i, _) ->
 127       let _, name, _, _ = L.nth us i in
 128       (name :: ss), name
 129    | C.Inductive (_, _, us, _), R.Con (i, j, _) ->
 130       let _, _, _, ts = L.nth us i in
 131       let _, name, _ = L.nth ts (pred j) in
 132       (name :: ss), name
 133    | C.Fixpoint (_, ts, _)    , R.Fix (i, _, _) ->
 134       let _, name, _, _, _ = L.nth ts i in
 135       (name :: ss), name
 136    | C.Fixpoint (_, ts, _)    , R.CoFix i       ->
 137       let _, name, _, _, _ = L.nth ts i in
 138       (name :: ss), name
 139    | _                                          ->
 140       failwith "name_of_reference"
 141
 142 let resolve_reference = function
 143    | R.Ref (u, r) ->
 144       let ss = segments_of_uri u in
 145       let _, _, _, _, obj = E.get_checked_obj G.status u in
 146       let ss, name = names_of_reference ss (obj, r) in
 147       X.rev_map_concat X.id "." "type" ss, name