X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=41802530bb2e004e8f68807ed9b552423885b770;hb=136fb0fde826e200ee8a0e902dbb6278b2afdeb8;hp=acb942ec5f37b9c4000a7b72c57e79a424b457eb;hpb=0568c864d39f55fd2a32382bf5bc163edc0284b0;p=helm.git diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index acb942ec5..41802530b 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -46,7 +46,7 @@ let rec force_does_not_occur 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 @@ -64,7 +64,6 @@ let rec force_does_not_occur subst to_be_restricted t = try Some (aux k t) with Occur -> -prerr_endline (Printf.sprintf "RESTRINGO (%d,%d)" n !i) ; more_to_be_restricted := (n,!i) :: !more_to_be_restricted; None) l @@ -122,10 +121,13 @@ let rec restrict subst to_be_restricted metasenv = 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 @@ -133,7 +135,7 @@ let rec restrict subst to_be_restricted metasenv = 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 @@ -153,27 +155,30 @@ 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' = + 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 @@ -182,6 +187,10 @@ 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 @@ -221,6 +230,14 @@ 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 + 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 @@ -477,25 +494,36 @@ let apply_subst_metasenv 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)) @@ -549,7 +577,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 = @@ -559,8 +591,26 @@ 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 + +(** {2 Format-like pretty printers} *) + +let fpp_gen ppf s = + Format.pp_print_string ppf s; + Format.pp_print_newline ppf (); + Format.pp_print_flush ppf () + +let fppsubst ppf subst = fpp_gen ppf (ppsubst subst) +let fppterm ppf term = fpp_gen ppf (CicPp.ppterm term) +let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv metasenv [])