let module C = Cic in
let more_to_be_restricted = ref [] in
let rec aux k = function
- C.Rel r when List.mem (r+k) to_be_restricted -> raise Occur
+ C.Rel r when List.mem (r - k) to_be_restricted -> raise Occur
| C.Rel _
| C.Sort _ as t -> t
| C.Implicit -> assert false
| C.Meta (n, l) ->
- (try
- aux k (CicSubstitution.lift_meta l (List.assoc n subst))
- with Not_found ->
- let l' =
- let i = ref 0 in
- List.map
- (function
- | None -> None
- | Some t ->
- incr i;
- try
- Some (aux k t)
- with Occur ->
- more_to_be_restricted := (n,!i) :: !more_to_be_restricted;
- None)
- l
- in
- C.Meta (n, l'))
+ (* we do not retrieve the term associated to ?n in subst since *)
+ (* in this way we can restrict if something goes wrong *)
+ let l' =
+ let i = ref 0 in
+ List.map
+ (function t ->
+ incr i ;
+ match t with
+ None -> None
+ | Some t ->
+ try
+ Some (aux k t)
+ with Occur ->
+ more_to_be_restricted := (n,!i) :: !more_to_be_restricted;
+ None)
+ l
+ in
+ C.Meta (n, l')
| C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
| C.Prod (name,so,dest) -> C.Prod (name, aux k so, aux (k+1) dest)
| C.Lambda (name,so,dest) -> C.Lambda (name, aux k so, aux (k+1) dest)
String.concat ", "
(List.map
(fun i ->
- match List.nth context i with
- | None -> assert false
- | Some (n, _) -> CicPp.ppname n)
- indexes)
+ try
+ match List.nth context i with
+ | None -> assert false
+ | Some (n, _) -> CicPp.ppname n
+ with
+ Failure _ -> assert false
+ ) indexes)
in
let force_does_not_occur_in_context to_be_restricted = function
| None -> [], None
let (more_to_be_restricted, t') =
force_does_not_occur subst to_be_restricted t
in
- more_to_be_restricted, Some (name, Cic.Decl t)
+ more_to_be_restricted, Some (name, Cic.Decl t')
| Some (name, Cic.Def (bo, ty)) ->
let (more_to_be_restricted, bo') =
force_does_not_occur subst to_be_restricted bo
let rec erase i to_be_restricted n = function
| [] -> [], to_be_restricted, []
| hd::tl ->
- let restrict_me = List.mem i to_be_restricted in
+ let more_to_be_restricted,restricted,tl' =
+ erase (i+1) to_be_restricted n tl
+ in
+ let restrict_me = List.mem i restricted in
if restrict_me then
- let more_to_be_restricted, restricted, new_tl =
- erase (i+1) (i :: to_be_restricted) n tl
- in
- more_to_be_restricted, restricted, None :: new_tl
+ more_to_be_restricted, restricted, None:: tl'
else
(try
- let more_to_be_restricted, hd' =
- force_does_not_occur_in_context to_be_restricted hd
- in
- let more_to_be_restricted', restricted, tl' =
- erase (i+1) to_be_restricted n tl
+ let more_to_be_restricted', hd' =
+ let delifted_restricted =
+ let rec aux =
+ function
+ [] -> []
+ | j::tl when j > i -> (j - i)::aux tl
+ | _::tl -> aux tl
+ in
+ aux restricted
+ in
+ force_does_not_occur_in_context delifted_restricted hd
in
- more_to_be_restricted @ more_to_be_restricted',
- restricted, hd' :: tl'
+ more_to_be_restricted @ more_to_be_restricted',
+ restricted, hd' :: tl'
with Occur ->
- let more_to_be_restricted, restricted, tl' =
- erase (i+1) (i :: to_be_restricted) n tl
- in
- more_to_be_restricted, restricted, None :: tl')
+ more_to_be_restricted, (i :: restricted), None :: tl')
in
let (more_to_be_restricted, metasenv, subst) =
List.fold_right
List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
in
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
try
"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
(CicPp.ppterm s)))
- with Not_found -> (more @ more_to_be_restricted, metasenv', subst))
+ with Not_found -> (more @ more_to_be_restricted @ more_to_be_restricted', metasenv', subst))
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"
(*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)
let delift n subst context metasenv l t =
- let l =
- let (_, canonical_context, _) = CicUtil.lookup_meta n metasenv in
- List.map2 (fun ct lt ->
- match (ct, lt) with
- | None, _ -> None
- | Some _, _ -> lt)
- canonical_context l
- in
let module S = CicSubstitution in
+ let l =
+ let (_, canonical_context, _) = CicUtil.lookup_meta n metasenv in
+ List.map2 (fun ct lt ->
+ match (ct, lt) with
+ | None, _ -> None
+ | Some _, _ -> lt)
+ canonical_context l
+ in
let to_be_restricted = ref [] in
let rec deliftaux k =
let module C = Cic in
"Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)"
i (CicPp.ppterm t)))
else
- (try
- deliftaux k (S.lift_meta l (List.assoc i subst))
- with Not_found ->
- let rec deliftl j =
- function
- [] -> []
- | None::tl -> None::(deliftl (j+1) tl)
- | (Some t)::tl ->
- let l1' = (deliftl (j+1) tl) in
- try
- Some (deliftaux k t)::l1'
- with
- NotInTheList
- | MetaSubstFailure _ ->
- to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
- in
- let l' = deliftl 1 l1 in
- C.Meta(i,l'))
+ (* I do not consider the term associated to ?i in subst since *)
+ (* in this way I can restrict if something goes wrong. *)
+ let rec deliftl j =
+ function
+ [] -> []
+ | None::tl -> None::(deliftl (j+1) tl)
+ | (Some t)::tl ->
+ let l1' = (deliftl (j+1) tl) in
+ try
+ Some (deliftaux k t)::l1'
+ with
+ NotInTheList
+ | MetaSubstFailure _ ->
+ to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
+ in
+ let l' = deliftl 1 l1 in
+ C.Meta(i,l')
| C.Sort _ as t -> t
| C.Implicit as t -> t
| C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
| None -> None :: context)
context []
+let apply_subst_metasenv subst 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))
+ metasenv)
+
let ppterm subst term = CicPp.ppterm (apply_subst subst term)
-let ppcontext ?(sep = "\n") subst context =
- String.concat sep
- (List.rev_map (function
- | Some (n, Cic.Decl t) ->
- sprintf "%s : %s" (CicPp.ppname n) (ppterm subst t)
- | Some (n, Cic.Def (t, ty)) ->
- sprintf "%s : %s := %s"
- (CicPp.ppname n)
- (match ty with None -> "_" | Some ty -> ppterm subst ty)
- (ppterm subst t)
- | None -> "_")
- context)
+let ppterm_in_context subst term name_context =
+ CicPp.pp (apply_subst subst term) name_context
+
+let ppcontext' ?(sep = "\n") subst context =
+ let separate s = if s = "" then "" else s ^ sep in
+ List.fold_right
+ (fun context_entry (i,name_context) ->
+ match context_entry with
+ Some (n,Cic.Decl t) ->
+ sprintf "%s%s : %s" (separate i) (CicPp.ppname n)
+ (ppterm_in_context subst t name_context), (Some n)::name_context
+ | Some (n,Cic.Def (bo,ty)) ->
+ sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n)
+ (match ty with
+ None -> "_"
+ | Some ty -> ppterm_in_context subst ty name_context)
+ (ppterm_in_context subst bo name_context), (Some n)::name_context
+ | None ->
+ sprintf "%s_ :? _" (separate i), None::name_context
+ ) context ("",[])
+
+let ppcontext ?sep subst context = fst (ppcontext' ?sep subst context)
let ppmetasenv ?(sep = "\n") metasenv subst =
String.concat sep
(List.map
(fun (i, c, t) ->
- sprintf "%s |- ?%d: %s" (ppcontext ~sep:"; " subst c) i
- (ppterm subst t))
+ let context,name_context = ppcontext' ~sep:"; " subst c in
+ 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))
metasenv))
let t2 = apply_subst subst t2 in
CicReduction.are_convertible context t1 t2
+let tempi_type_of_aux_subst = ref 0.0;;
+let tempi_type_of_aux = ref 0.0;;
+
let type_of_aux' metasenv subst context term =
+let time1 = Unix.gettimeofday () in
let term = apply_subst subst term in
let context = apply_subst_context subst context in
let metasenv =
(fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) 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 time3 = Unix.gettimeofday () in
+ tempi_type_of_aux_subst := !tempi_type_of_aux_subst +. time3 -. time1 ;
+ tempi_type_of_aux := !tempi_type_of_aux +. time2 -. time1 ;
+ res
projects / helm.git / blobdiff