let module R = CicReduction in
let module U = UriManager in
let cobj,ugraph =
- match CicEnvironment.is_type_checked ~trust:true uri ugraph with
+ match CicEnvironment.is_type_checked ~trust:true ugraph uri with
CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
| CicEnvironment.UncheckedObj uobj ->
logger#log (`Start_type_checking uri) ;
try
CicEnvironment.set_type_checking_info uri;
logger#log (`Type_checking_completed uri) ;
- match CicEnvironment.is_type_checked ~trust:false uri ugraph with
+ match CicEnvironment.is_type_checked ~trust:false ugraph uri with
CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
| CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
with Invalid_argument s ->
let module R = CicReduction in
let module U = UriManager in
(* 0 because a variable is never cooked => no partial cooking at one level *)
- match CicEnvironment.is_type_checked ~trust:true uri ugraph with
+ match CicEnvironment.is_type_checked ~trust:true ugraph uri with
CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_)),ugraph') -> ty,ugraph'
| CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_)) ->
logger#log (`Start_type_checking uri) ;
(try
CicEnvironment.set_type_checking_info uri ;
logger#log (`Type_checking_completed uri) ;
- match CicEnvironment.is_type_checked ~trust:false uri ugraph with
+ match CicEnvironment.is_type_checked ~trust:false ugraph uri with
CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_)),ugraph') ->
ty,ugraph'
| CicEnvironment.CheckedObj _
List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
| C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) ->
let (ok,paramsno,ity,cl,name) =
- let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
C.InductiveDefinition (tl,_,paramsno) ->
let (name,_,ity,cl) = List.nth tl i in
let module R = CicReduction in
let module U = UriManager in
let cobj,ugraph1 =
- match CicEnvironment.is_type_checked ~trust:true uri ugraph with
+ match CicEnvironment.is_type_checked ~trust:true ugraph uri with
CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
| CicEnvironment.UncheckedObj uobj ->
logger#log (`Start_type_checking uri) ;
try
CicEnvironment.set_type_checking_info uri ;
logger#log (`Type_checking_completed uri) ;
- (match CicEnvironment.is_type_checked ~trust:false uri ugraph with
+ (match CicEnvironment.is_type_checked ~trust:false ugraph uri with
CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,ugraph')
| CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
)
let module R = CicReduction in
let module U = UriManager in
let cobj,ugraph1 =
- match CicEnvironment.is_type_checked ~trust:true uri ugraph with
+ match CicEnvironment.is_type_checked ~trust:true ugraph uri with
CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
| CicEnvironment.UncheckedObj uobj ->
logger#log (`Start_type_checking uri) ;
try
CicEnvironment.set_type_checking_info uri ;
logger#log (`Type_checking_completed uri) ;
- (match CicEnvironment.is_type_checked
- ~trust:false uri ugraph with
- CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
- | CicEnvironment.UncheckedObj _ ->
+ (match
+ CicEnvironment.is_type_checked ~trust:false ugraph uri
+ with
+ CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
+ | CicEnvironment.UncheckedObj _ ->
raise CicEnvironmentError)
with
Invalid_argument s ->
(match term with
C.Rel m when List.mem m safes || m = x ->
let (tys,len,isinductive,paramsno,cl) =
- let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
C.InductiveDefinition (tl,_,paramsno) ->
let tys =
) (List.combine pl cl) true
| C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
let (tys,len,isinductive,paramsno,cl) =
- let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
C.InductiveDefinition (tl,_,paramsno) ->
let (_,isinductive,_,cl) = List.nth tl i in
(match term with
C.Rel m when List.mem m safes || m = x ->
let (tys,len,isinductive,paramsno,cl) =
- let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
C.InductiveDefinition (tl,_,paramsno) ->
let len = List.length tl in
) (List.combine pl cl) true
| C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
let (tys,len,isinductive,paramsno,cl) =
- let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
C.InductiveDefinition (tl,_,paramsno) ->
let (_,isinductive,_,cl) = List.nth tl i in
let consty =
let obj,_ =
try
- CicEnvironment.get_cooked_obj ~trust:false uri CicUniv.empty_ugraph
+ CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
with Not_found -> assert false
in
match obj with
| (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy ->
(* TASSI: da verificare *)
(*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
- (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
C.InductiveDefinition (itl,_,_) ->
let (_,_,_,cl) = List.nth itl i in
| ((C.Sort C.Set, C.Sort (C.Type _)) | (C.Sort C.CProp, C.Sort (C.Type _)))
(* TASSI: da verificare *)
when need_dummy ->
- (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
C.InductiveDefinition (itl,_,paramsno) ->
let tys =
(match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
C.Sort C.Prop -> true,ugraph1
| (C.Sort C.Set | C.Sort C.CProp) ->
- (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
C.InductiveDefinition (itl,_,_) ->
let (_,_,_,cl) = List.nth itl i in
| C.Sort C.CProp -> true,ugraph1
| C.Sort (C.Type _) ->
(* TASSI: da verificare *)
- (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
C.InductiveDefinition (itl,_,paramsno) ->
let (_,_,_,cl) = List.nth itl i in
let parsno =
let obj,_ =
try
- CicEnvironment.get_cooked_obj ~trust:false uri CicUniv.empty_ugraph
+ CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
with Not_found -> assert false
in
match obj with
(*CSC: definire una funzioncina per questo codice sempre replicato *)
let obj,_ =
try
- CicEnvironment.get_cooked_obj ~trust:false uri CicUniv.empty_ugraph
+ CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
with Not_found -> assert false
in
(match obj with
UriManager.string_of_uri uri))
)
| C.Appl ((C.MutInd (uri,i,_))::_) ->
- (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
C.InductiveDefinition (itl,_,_) ->
let (_,is_inductive,_,_) = List.nth itl i in
let module U = UriManager in
let logger = new CicLogger.logger in
(* ??? match CicEnvironment.is_type_checked ~trust:true uri with ???? *)
- match CicEnvironment.is_type_checked ~trust:false uri ugraph with
+ match CicEnvironment.is_type_checked ~trust:false ugraph uri with
CicEnvironment.CheckedObj (cobj,ugraph') ->
(* prerr_endline ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*)
cobj,ugraph'
try
CicEnvironment.set_type_checking_info uri;
logger#log (`Type_checking_completed uri);
- match CicEnvironment.is_type_checked ~trust:false uri ugraph with
+ match CicEnvironment.is_type_checked ~trust:false ugraph uri with
CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
| _ -> raise CicEnvironmentError
with