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