From: Claudio Sacerdoti Coen Date: Thu, 5 Feb 2004 10:33:59 +0000 (+0000) Subject: Bug fixed: the canonical contexts were traversed in the wrong direction X-Git-Tag: V_0_2_3~56 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d81c44634c85266ba2dd5b24a68ee6780234953a;p=helm.git Bug fixed: the canonical contexts were traversed in the wrong direction during restriction. As a consequence, some hypothesis were not correctly restricted. --- diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index 30069cdfe..aed59c5f4 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -42,11 +42,11 @@ let position n = exception Occur;; -let rec force_does_not_occur subst to_be_restricted t = +let rec force_does_not_occur k subst to_be_restricted t = 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 @@ -113,7 +113,7 @@ let rec force_does_not_occur subst to_be_restricted t = in C.CoFix (i, fl') in - let res = aux 0 t in + let res = aux k t in (!more_to_be_restricted, res) let rec restrict subst to_be_restricted metasenv = @@ -126,23 +126,23 @@ let rec restrict subst to_be_restricted metasenv = | Some (n, _) -> CicPp.ppname n) indexes) in - let force_does_not_occur_in_context to_be_restricted = function + let force_does_not_occur_in_context k to_be_restricted = function | None -> [], None | Some (name, Cic.Decl t) -> let (more_to_be_restricted, t') = - force_does_not_occur subst to_be_restricted t + force_does_not_occur k 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 + force_does_not_occur k subst to_be_restricted bo in let more_to_be_restricted, ty' = match ty with | None -> more_to_be_restricted, None | Some ty -> let more_to_be_restricted', ty' = - force_does_not_occur subst to_be_restricted ty + force_does_not_occur k subst to_be_restricted ty in more_to_be_restricted @ more_to_be_restricted', Some ty' @@ -152,27 +152,21 @@ let rec restrict subst to_be_restricted metasenv = 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' = + force_does_not_occur_in_context i 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 @@ -181,18 +175,22 @@ let rec restrict subst to_be_restricted metasenv = 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 let more_to_be_restricted', t' = - force_does_not_occur subst restricted t + force_does_not_occur 0 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 + force_does_not_occur 0 subst restricted s in let subst' = (n, s') :: (List.remove_assoc n subst) in let more = @@ -220,6 +218,16 @@ let rec restrict subst to_be_restricted metasenv = (*CSC: maybe we should rename delift in abstract, as I did in my dissertation *) let delift n subst context metasenv l t = let module S = CicSubstitution in +(* THIS CODE SHOULD NOT BE USEFUL AT ALL + 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 @@ -559,7 +567,11 @@ let are_convertible subst context t1 t2 = 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 = @@ -569,8 +581,14 @@ let type_of_aux' metasenv subst context term = (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