helm/software/components/ng_kernel/nCicEnvironment.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 (* $Id$ *)
  13
  14 exception CircularDependency of string Lazy.t;;
  15 exception ObjectNotFound of string Lazy.t;;
  16 exception BadDependency of string Lazy.t;;
  17
  18 let typecheck_obj,already_set = ref (fun _ -> assert false), ref false;;
  19 let set_typecheck_obj f =
  20  if !already_set then
  21   assert false
  22  else
  23   begin
  24    typecheck_obj := f;
  25    already_set := true
  26   end
  27 ;;
  28
  29 let cache = NUri.UriHash.create 313;;
  30 let frozen_list = ref [];;
  31
  32 exception Propagate of NUri.uri * exn;;
  33
  34 let get_checked_obj u =
  35  if List.exists (fun (k,_) -> NUri.eq u k) !frozen_list
  36  then
  37   raise (CircularDependency (lazy (NUri.string_of_uri u)))
  38  else
  39   let obj =
  40    try NUri.UriHash.find cache u
  41    with
  42     Not_found ->
  43      let saved_frozen_list = !frozen_list in
  44      try
  45       let obj =
  46        try NCicLibrary.get_obj u
  47        with
  48         NCicLibrary.ObjectNotFound m -> raise (ObjectNotFound m)
  49       in
  50         frozen_list := (u,obj)::saved_frozen_list;
  51         !typecheck_obj obj;
  52         frozen_list := saved_frozen_list;
  53         let obj = `WellTyped obj in
  54         NUri.UriHash.add cache u obj;
  55         obj
  56      with
  57         Sys.Break as e ->
  58          frozen_list := saved_frozen_list;
  59          raise e
  60       | Propagate (u',_) as e' ->
  61          frozen_list := saved_frozen_list;
  62          let exn = `Exn (BadDependency (lazy (NUri.string_of_uri u ^
  63            " depends (recursively) on " ^ NUri.string_of_uri u' ^
  64            " which is not well-typed"))) in
  65          NUri.UriHash.add cache u exn;
  66          if saved_frozen_list = [] then
  67           exn
  68          else
  69           raise e'
  70       | e ->
  71          frozen_list := saved_frozen_list;
  72          let exn = `Exn e in
  73          NUri.UriHash.add cache u exn;
  74          if saved_frozen_list = [] then
  75           exn
  76          else
  77           raise (Propagate (u,e))
  78   in
  79    match obj with
  80       `WellTyped o -> o
  81     | `Exn e -> raise e
  82 ;;
  83
  84 let get_checked_def = function
  85   | NReference.Ref (_, uri, NReference.Def) ->
  86       (match get_checked_obj uri with
  87       | _,height,_,_, NCic.Constant (rlv,name,Some bo,ty,att) ->
  88           rlv,name,bo,ty,att,height
  89       | _,_,_,_, NCic.Constant (_,_,None,_,_) ->
  90           prerr_endline "get_checked_def on an axiom"; assert false
  91       | _ -> prerr_endline "get_checked_def on a non def 2"; assert false)
  92   | _ -> prerr_endline "get_checked_def on a non def"; assert false
  93 ;;
  94
  95 let get_checked_indtys = function
  96   | NReference.Ref (_, uri, (NReference.Ind (_,n)|NReference.Con (n,_))) ->
  97       (match get_checked_obj uri with
  98       | _,_,_,_, NCic.Inductive (inductive,leftno,tys,att) ->
  99         inductive,leftno,tys,att,n
 100       | _ -> prerr_endline "get_checked_indtys on a non ind 2"; assert false)
 101   | _ -> prerr_endline "get_checked_indtys on a non ind"; assert false
 102 ;;
 103
 104 let get_checked_fixes_or_cofixes = function
 105   | NReference.Ref (_, uri, (NReference.Fix (fixno,_)|NReference.CoFix fixno))->
 106       (match get_checked_obj uri with
 107       | _,height,_,_, NCic.Fixpoint (_,funcs,att) ->
 108          funcs, att, height
 109       | _ ->prerr_endline "get_checked_(co)fix on a non (co)fix 2";assert false)
 110   | r -> prerr_endline ("get_checked_(co)fix on " ^ NReference.string_of_reference r); assert false
 111 ;;
 112
 113 let get_indty_leftno = function
 114   | NReference.Ref (_, uri, NReference.Ind _)
 115   | NReference.Ref (_, uri, NReference.Con _) ->
 116       (match get_checked_obj uri with
 117       | _,_,_,_, NCic.Inductive (_,left,_,_) -> left
 118       | _ ->prerr_endline "get_indty_leftno called on a non ind 2";assert false)
 119   | _ -> prerr_endline "get_indty_leftno called on a non indty";assert false
 120 ;;
 121
 122 let invalidate _ =
 123   assert (!frozen_list = []);
 124   NUri.UriHash.clear cache
 125 ;;