open Printf
+let apply_subst_counter = ref 0
+let apply_subst_context_counter = ref 0
+let apply_subst_metasenv_counter = ref 0
+let lift_counter = ref 0
+let subst_counter = ref 0
+let whd_counter = ref 0
+let are_convertible_counter = ref 0
+let metasenv_length = ref 0
+let context_length = ref 0
+
+let reset_counters () =
+ apply_subst_counter := 0;
+ apply_subst_context_counter := 0;
+ apply_subst_metasenv_counter := 0;
+ lift_counter := 0;
+ subst_counter := 0;
+ whd_counter := 0;
+ are_convertible_counter := 0;
+ metasenv_length := 0;
+ context_length := 0
+
+let print_counters () =
+ prerr_endline (Printf.sprintf
+"apply_subst: %d
+apply_subst_context: %d
+apply_subst_metasenv: %d
+lift: %d
+subst: %d
+whd: %d
+are_convertible: %d
+metasenv length: %d (avg = %.2f)
+context length: %d (avg = %.2f)
+"
+ !apply_subst_counter !apply_subst_context_counter
+ !apply_subst_metasenv_counter !lift_counter !subst_counter !whd_counter
+ !are_convertible_counter !metasenv_length
+ ((float !metasenv_length) /. (float !apply_subst_metasenv_counter))
+ !context_length
+ ((float !context_length) /. (float !apply_subst_context_counter))
+ )
exception MetaSubstFailure of string
exception Uncertain of string
exception AssertFailure of string
+exception SubstNotFound of int
let debug_print = prerr_endline
-type substitution = (int * Cic.term) list
+type substitution = (int * (Cic.context * Cic.term)) list
+
+let lookup_subst n subst =
+ try
+ List.assoc n subst
+ with Not_found -> raise (SubstNotFound n)
(*** Functions to apply a substitution ***)
C.Var (uri, exp_named_subst')
| C.Meta (i, l) ->
(try
- let t = List.assoc i subst in
+ let (context, t) = lookup_subst i subst in
um_aux (S.lift_meta l t)
- with Not_found -> (* not constrained variable, i.e. free in subst*)
+ with SubstNotFound _ -> (* unconstrained variable, i.e. free in subst*)
let l' =
List.map (function None -> None | Some t -> Some (um_aux t)) l
in
| _ -> t'
end
in
- apply_subst_gen ~appl_fun
+ fun s t ->
+ incr apply_subst_counter;
+ apply_subst_gen ~appl_fun s t
;;
let rec apply_subst_context subst context =
+ incr apply_subst_context_counter;
+ context_length := !context_length + List.length context;
List.fold_right
(fun item context ->
match item with
context []
let apply_subst_metasenv subst metasenv =
+ incr apply_subst_metasenv_counter;
+ metasenv_length := !metasenv_length + List.length metasenv;
List.map
(fun (n, context, ty) ->
(n, apply_subst_context subst context, apply_subst subst ty))
(List.filter
- (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
+ (fun (i, _, _) -> not (List.mem_assoc i subst))
metasenv)
(***** Pretty printing functions ******)
let ppsubst subst =
String.concat "\n"
(List.map
- (fun (idx, term) -> Printf.sprintf "?%d := %s" idx (CicPp.ppterm term))
+ (fun (idx, (_, term)) ->
+ Printf.sprintf "?%d := %s" idx (CicPp.ppterm term))
subst)
;;
sprintf "%s |- ?%d: %s" context i
(ppterm_in_context subst t name_context))
(List.filter
- (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
+ (fun (i, _, _) -> not (List.mem_assoc i subst))
metasenv))
(* From now on we recreate a kernel abstraction where substitutions are part of
* the calculus *)
let lift subst n term =
+ incr subst_counter;
let term = apply_subst subst term in
try
CicSubstitution.lift n term
raise (MetaSubstFailure ("Lift failure: " ^ Printexc.to_string e))
let subst subst t1 t2 =
+ incr subst_counter;
let t1 = apply_subst subst t1 in
let t2 = apply_subst subst t2 in
try
raise (MetaSubstFailure ("Subst failure: " ^ Printexc.to_string e))
let whd subst context term =
+ incr whd_counter;
let term = apply_subst subst term in
let context = apply_subst_context subst context in
try
Printexc.to_string e))
let are_convertible subst context t1 t2 =
+ incr are_convertible_counter;
let context = apply_subst_context subst context in
let t1 = apply_subst subst t1 in
let t2 = apply_subst subst t2 in
let tempi_subst = ref 0.0;;
let tempi_type_of_aux = ref 0.0;;
+ (* assumption: metasenv is already instantiated wrt subst *)
let type_of_aux' metasenv subst context term =
-let time1 = Unix.gettimeofday () in
+ let time1 = Unix.gettimeofday () in
let term = apply_subst subst term in
let context = apply_subst_context subst context in
- let metasenv =
- List.map
- (fun (i, c, t) -> (i, apply_subst_context subst c, apply_subst subst t))
- (List.filter
- (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
- metasenv)
+(* let metasenv = apply_subst_metasenv subst metasenv in *)
+ let time2 = Unix.gettimeofday () in
+ let res =
+ try
+ CicTypeChecker.type_of_aux' metasenv context term
+ with CicTypeChecker.TypeCheckerFailure msg ->
+ raise (MetaSubstFailure ("Type checker failure: " ^ msg))
in
-let time2 = Unix.gettimeofday () in
-let res =
- try
- CicTypeChecker.type_of_aux' metasenv context term
- with CicTypeChecker.TypeCheckerFailure msg ->
- raise (MetaSubstFailure ("Type checker failure: " ^ msg))
-in
-let time3 = Unix.gettimeofday () in
- tempi_type_of_aux_subst := !tempi_type_of_aux_subst +. time3 -. time1 ;
- tempi_subst := !tempi_subst +. time2 -. time1 ;
- tempi_type_of_aux := !tempi_type_of_aux +. time3 -. time2 ;
- res
+ let time3 = Unix.gettimeofday () in
+ tempi_type_of_aux_subst := !tempi_type_of_aux_subst +. time3 -. time1 ;
+ tempi_subst := !tempi_subst +. time2 -. time1 ;
+ tempi_type_of_aux := !tempi_type_of_aux +. time3 -. time2 ;
+ res
(**** DELIFT ****)
(* the delift function takes in input a metavariable index, an ordered list of
with Occur ->
more_to_be_restricted, (i :: restricted), None :: tl')
in
- let (more_to_be_restricted, metasenv, subst) =
+ let (more_to_be_restricted, metasenv) = (* restrict metasenv *)
List.fold_right
- (fun (n, context, t) (more, metasenv, subst) ->
+ (fun (n, context, t) (more, metasenv) ->
let to_be_restricted =
List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
in
force_does_not_occur subst restricted t
in
let metasenv' = (n, context', t') :: metasenv in
- (try
- let s = List.assoc n subst in
- try
- let more_to_be_restricted'', s' =
- force_does_not_occur subst restricted s
- in
- let subst' = (n, s') :: (List.remove_assoc n subst) in
- let more =
- more @ more_to_be_restricted @ more_to_be_restricted' @
- more_to_be_restricted''
- in
- (more, metasenv', subst')
- with Occur ->
- raise (MetaSubstFailure (sprintf
- "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term"
- n (names_of_context_indexes context to_be_restricted) n
- (ppterm subst s)))
- with Not_found -> (more @ more_to_be_restricted @ more_to_be_restricted', metasenv', subst))
+ (more @ more_to_be_restricted @ more_to_be_restricted',
+ metasenv')
with Occur ->
raise (MetaSubstFailure (sprintf
"Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them"
n (names_of_context_indexes context to_be_restricted))))
- metasenv ([], [], subst)
+ metasenv ([], [])
+ in
+ let (more_to_be_restricted', subst) = (* restrict subst *)
+ List.fold_right
+ (fun (n, (context, term)) (more, subst) ->
+ let to_be_restricted =
+ List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
+ in
+ (try
+ let (more_to_be_restricted, restricted, context') =
+ (* just an optimization *)
+ if to_be_restricted = [] then
+ [], [], context
+ else
+ erase 1 to_be_restricted n context
+ in
+ let more_to_be_restricted', term' =
+ force_does_not_occur subst restricted term
+ in
+ let subst' = (n, (context', term')) :: subst in
+ let more = more @ more_to_be_restricted @ more_to_be_restricted' in
+ (more, subst')
+ with Occur ->
+ raise (MetaSubstFailure (sprintf
+ "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term"
+ n (names_of_context_indexes context to_be_restricted) n
+ (ppterm subst term)))))
+ subst ([], [])
in
- match more_to_be_restricted with
+ match more_to_be_restricted @ more_to_be_restricted' with
| [] -> (metasenv, subst)
- | _ -> restrict subst more_to_be_restricted metasenv
+ | l -> restrict subst l metasenv
;;
(*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)
projects / helm.git / blobdiff