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_decl = function
  85   | NReference.Ref (uri, NReference.Decl) ->
  86       (match get_checked_obj uri with
  87       | _,height,_,_, NCic.Constant (rlv,name,None,ty,att) ->
  88           rlv,name,ty,att,height
  89       | _,_,_,_, NCic.Constant (_,_,Some _,_,_) ->
  90           prerr_endline "get_checked_decl on a definition"; assert false
  91       | _ -> prerr_endline "get_checked_decl on a non decl 2"; assert false)
  92   | _ -> prerr_endline "get_checked_decl on a non decl"; assert false
  93 ;;
  94
  95 let get_checked_def = function
  96   | NReference.Ref (uri, NReference.Def _) ->
  97       (match get_checked_obj uri with
  98       | _,height,_,_, NCic.Constant (rlv,name,Some bo,ty,att) ->
  99           rlv,name,bo,ty,att,height
 100       | _,_,_,_, NCic.Constant (_,_,None,_,_) ->
 101           prerr_endline "get_checked_def on an axiom"; assert false
 102       | _ -> prerr_endline "get_checked_def on a non def 2"; assert false)
 103   | _ -> prerr_endline "get_checked_def on a non def"; assert false
 104 ;;
 105
 106 let get_checked_indtys = function
 107   | NReference.Ref (uri, (NReference.Ind (_,n)|NReference.Con (n,_))) ->
 108       (match get_checked_obj uri with
 109       | _,_,_,_, NCic.Inductive (inductive,leftno,tys,att) ->
 110         inductive,leftno,tys,att,n
 111       | _ -> prerr_endline "get_checked_indtys on a non ind 2"; assert false)
 112   | _ -> prerr_endline "get_checked_indtys on a non ind"; assert false
 113 ;;
 114
 115 let get_checked_fixes_or_cofixes = function
 116   | NReference.Ref (uri, (NReference.Fix (fixno,_,_)|NReference.CoFix fixno))->
 117       (match get_checked_obj uri with
 118       | _,height,_,_, NCic.Fixpoint (_,funcs,att) ->
 119          funcs, att, height
 120       | _ ->prerr_endline "get_checked_(co)fix on a non (co)fix 2";assert false)
 121   | r -> prerr_endline ("get_checked_(co)fix on " ^ NReference.string_of_reference r); assert false
 122 ;;
 123
 124 let get_indty_leftno = function
 125   | NReference.Ref (uri, NReference.Ind _)
 126   | NReference.Ref (uri, NReference.Con _) ->
 127       (match get_checked_obj uri with
 128       | _,_,_,_, NCic.Inductive (_,left,_,_) -> left
 129       | _ ->prerr_endline "get_indty_leftno called on a non ind 2";assert false)
 130   | _ -> prerr_endline "get_indty_leftno called on a non indty";assert false
 131 ;;
 132
 133 let get_relevance (NReference.Ref (_, infos) as r) =
 134   match infos with
 135      NReference.Def _ -> let res,_,_,_,_,_ = get_checked_def r in res
 136    | NReference.Decl -> let res,_,_,_,_ = get_checked_decl r in res
 137    | NReference.Ind _ ->
 138        let _,_,tl,_,n = get_checked_indtys r in
 139        let res,_,_,_ = List.nth tl n in
 140          res
 141     | NReference.Con (_,i) ->
 142        let _,_,tl,_,n = get_checked_indtys r in
 143        let _,_,_,cl = List.nth tl n in
 144        let res,_,_ = List.nth cl (i - 1) in
 145          res
 146     | NReference.Fix (fixno,_,_)
 147     | NReference.CoFix fixno ->
 148         let fl,_,_ = get_checked_fixes_or_cofixes r in
 149         let res,_,_,_,_ = List.nth fl fixno in
 150           res
 151 ;;
 152
 153
 154 let invalidate _ =
 155   assert (!frozen_list = []);
 156   NUri.UriHash.clear cache
 157 ;;