raise (TypeCheckerFailure (List.fold_right debug_aux (t::context) ""))
;;
-let debug_print = prerr_endline ;;
+let debug_print = fun _ -> () ;;
let rec split l n =
match (l,n) with
CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
| CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
with Invalid_argument s ->
- (*prerr_endline s;*)
+ (*debug_print s;*)
uobj,ugraph_dust
in
match cobj,ugraph with
| CicEnvironment.CheckedObj _
| CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
with Invalid_argument s ->
- (*prerr_endline s;*)
+ (*debug_print s;*)
ty,ugraph2)
| _ ->
raise (TypeCheckerFailure ("Unknown variable:" ^ U.string_of_uri uri))
)
with
Invalid_argument s ->
- (*prerr_endline s;*)
+ (*debug_print s;*)
uobj,ugraph1_dust
in
match cobj with
raise CicEnvironmentError)
with
Invalid_argument s ->
- (*prerr_endline s;*)
+ (*debug_print s;*)
uobj,ugraph1_dust
in
match cobj with
function
[] -> []
| (Some (n,C.Decl t))::tl ->
- (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+ (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
| (Some (n,C.Def (t,None)))::tl ->
- (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
+ (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
| None::tl -> None::(aux (i+1) tl)
| (Some (n,C.Def (t,Some ty)))::tl ->
- (Some (n,C.Def ((S.lift_meta l (S.lift i t)),Some (S.lift_meta l (S.lift i ty)))))::(aux (i+1) tl)
+ (Some (n,C.Def ((S.subst_meta l (S.lift i t)),Some (S.subst_meta l (S.lift i ty)))))::(aux (i+1) tl)
in
aux 1 canonical_context
in
~subst metasenv context canonical_context l ugraph
in
(* assuming subst is well typed !!!!! *)
- ((CicSubstitution.lift_meta l ty), ugraph1)
- (* type_of_aux context (CicSubstitution.lift_meta l term) *)
+ ((CicSubstitution.subst_meta l ty), ugraph1)
+ (* type_of_aux context (CicSubstitution.subst_meta l term) *)
with CicUtil.Subst_not_found _ ->
let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
let ugraph1 =
check_metasenv_consistency ~logger
~subst metasenv context canonical_context l ugraph
in
- ((CicSubstitution.lift_meta l ty),ugraph1))
+ ((CicSubstitution.subst_meta l ty),ugraph1))
(* TASSI: CONSTRAINTS *)
| C.Sort (C.Type t) ->
let t' = CicUniv.fresh() in
(* ??? match CicEnvironment.is_type_checked ~trust:true uri 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);*)
+ (* debug_print ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*)
cobj,ugraph'
| CicEnvironment.UncheckedObj uobj ->
(* let's typecheck the uncooked object *)
logger#log (`Start_type_checking uri) ;
- (* prerr_endline ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *)
+ (* debug_print ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *)
let ugraph1 =
(match uobj with
C.Constant (_,Some te,ty,_,_) ->
object.
*)
Invalid_argument s ->
- (*prerr_endline s;*)
+ (*debug_print s;*)
uobj,ugraph1
;;