X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.ml;h=26dc85cacebadc948661b90ae084159a7499ba78;hb=c22f39a5d5afc0ef55beb221e00e2e6703b13d90;hp=4441fa16921b0852410b5a83c408dcc95f72f4df;hpb=c5b3da2ed2b2dafd22cc50edb4ac5f1d402dfa94;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index 4441fa169..26dc85cac 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -11,920 +11,467 @@ (* $Id$ *) - -(*open Printf - -(* PROFILING *) -(* -let deref_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 () = - debug_print (lazy (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 Lazy.t exception Uncertain of string Lazy.t -exception AssertFailure of string Lazy.t -exception DeliftingARelWouldCaptureAFreeVariable;; - -let debug_print = fun _ -> () -type substitution = (int * (Cic.context * Cic.term)) list - -(* -let rec deref subst = - let third _,_,a = a in - function - Cic.Meta(n,l) as t -> - (try - deref subst - (CicSubstitution.subst_meta - l (third (CicUtil.lookup_subst n subst))) - with - CicUtil.Subst_not_found _ -> t) - | t -> t +let newmeta,maxmeta = + let maxmeta = ref 0 in + (fun () -> incr maxmeta; !maxmeta), + (fun () -> !maxmeta) ;; -*) -let lookup_subst = CicUtil.lookup_subst -;; - -(* clean_up_meta take a metasenv and a term and make every local context -of each occurrence of a metavariable consistent with its canonical context, -with respect to the hidden hipothesis *) - -(* -let clean_up_meta subst metasenv t = - let module C = Cic in - let rec aux t = - match t with - C.Rel _ - | C.Sort _ -> t - | C.Implicit _ -> assert false - | C.Meta (n,l) as t -> - let cc = - (try - let (cc,_) = lookup_subst n subst in cc - with CicUtil.Subst_not_found _ -> - try - let (_,cc,_) = CicUtil.lookup_meta n metasenv in cc - with CicUtil.Meta_not_found _ -> assert false) in - let l' = - (try - List.map2 - (fun t1 t2 -> - match t1,t2 with - None , _ -> None - | _ , t -> t) cc l - with - Invalid_argument _ -> assert false) in - C.Meta (n, l') - | C.Cast (te,ty) -> C.Cast (aux te, aux ty) - | C.Prod (name,so,dest) -> C.Prod (name, aux so, aux dest) - | C.Lambda (name,so,dest) -> C.Lambda (name, aux so, aux dest) - | C.LetIn (name,so,dest) -> C.LetIn (name, aux so, aux dest) - | C.Appl l -> C.Appl (List.map aux l) - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst - in - C.Var (uri, exp_named_subst') - | C.Const (uri, exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst - in - C.Const (uri, exp_named_subst') - | C.MutInd (uri,tyno,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst - in - C.MutInd (uri, tyno, exp_named_subst') - | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst - in - C.MutConstruct (uri, tyno, consno, exp_named_subst') - | C.MutCase (uri,tyno,out,te,pl) -> - C.MutCase (uri, tyno, aux out, aux te, List.map aux pl) - | C.Fix (i,fl) -> - let fl' = - List.map - (fun (name,j,ty,bo) -> (name, j, aux ty, aux bo)) fl - in - C.Fix (i, fl') - | C.CoFix (i,fl) -> - let fl' = - List.map - (fun (name,ty,bo) -> (name, aux ty, aux bo)) fl - in - C.CoFix (i, fl') - in - aux t *) - -(*** Functions to apply a substitution ***) +exception NotInTheList;; -let apply_subst_gen ~appl_fun subst term = - let rec um_aux = - let module C = Cic in - let module S = CicSubstitution in - function - C.Rel _ as t -> t - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst - in - C.Var (uri, exp_named_subst') - | C.Meta (i, l) -> - (try - let (_, t,_) = lookup_subst i subst in - um_aux (S.subst_meta l t) - with CicUtil.Subst_not_found _ -> - (* unconstrained variable, i.e. free in subst*) - let l' = - List.map (function None -> None | Some t -> Some (um_aux t)) l - in - C.Meta (i,l')) - | C.Sort _ - | C.Implicit _ as t -> t - | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty) - | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t) - | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t) - | C.LetIn (n,s,ty,t) -> C.LetIn (n, um_aux s, um_aux ty, um_aux t) - | C.Appl (hd :: tl) -> appl_fun um_aux hd tl - | C.Appl _ -> assert false - | C.Const (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst - in - C.Const (uri, exp_named_subst') - | C.MutInd (uri,typeno,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst - in - C.MutInd (uri,typeno,exp_named_subst') - | C.MutConstruct (uri,typeno,consno,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst - in - C.MutConstruct (uri,typeno,consno,exp_named_subst') - | C.MutCase (sp,i,outty,t,pl) -> - let pl' = List.map um_aux pl in - C.MutCase (sp, i, um_aux outty, um_aux t, pl') - | C.Fix (i, fl) -> - let fl' = - List.map (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo)) fl - in - C.Fix (i, fl') - | C.CoFix (i, fl) -> - let fl' = - List.map (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo)) fl - in - C.CoFix (i, fl') - in - um_aux term +let position to_skip n (shift, lc) = + match lc with + | NCic.Irl _ when to_skip > 0 -> assert false (* unclear to me *) + | NCic.Irl len when n <= shift || n > shift + len -> raise NotInTheList + | NCic.Irl _ -> n - shift + | NCic.Ctx tl -> + let rec aux to_skip k = function + | [] -> raise NotInTheList + | _ :: tl when to_skip > 0 -> aux (to_skip - 1) (k+1) tl + | (NCic.Rel m)::_ when m + shift = n -> k + | _::tl -> aux to_skip (k+1) tl + in + aux to_skip 1 tl ;; -let apply_subst = - let appl_fun um_aux he tl = - let tl' = List.map um_aux tl in - let t' = - match um_aux he with - Cic.Appl l -> Cic.Appl (l@tl') - | he' -> Cic.Appl (he'::tl') - in - begin - match he with - Cic.Meta (m,_) -> CicReduction.head_beta_reduce t' - | _ -> t' - end +let pack_lc orig = + let rec are_contiguous k = function + | [] -> true + | (NCic.Rel j) :: tl when j = k+1 -> are_contiguous j tl + | _ -> false in - fun subst t -> -(* incr apply_subst_counter; *) -match subst with - [] -> t - | _ -> apply_subst_gen ~appl_fun subst t + match orig with + | _, NCic.Ctx [] -> 0, NCic.Irl 0 + | shift, NCic.Ctx (NCic.Rel k::tl as l) when are_contiguous k tl -> + shift+k-1, NCic.Irl (List.length l) + | _ -> orig ;; -let profiler = HExtlib.profile "U/CicMetaSubst.apply_subst" -let apply_subst s t = - profiler.HExtlib.profile (apply_subst s) t -let apply_subst_context subst context = - match subst with - [] -> context - | _ -> -(* - incr apply_subst_context_counter; - context_length := !context_length + List.length context; -*) - List.fold_right - (fun item context -> - match item with - | Some (n, Cic.Decl t) -> - let t' = apply_subst subst t in - Some (n, Cic.Decl t') :: context - | Some (n, Cic.Def (t, ty)) -> - let ty' = apply_subst subst ty in - let t' = apply_subst subst t in - Some (n, Cic.Def (t', ty')) :: context - | None -> None :: context) - context [] - -let apply_subst_metasenv subst metasenv = -(* - incr apply_subst_metasenv_counter; - metasenv_length := !metasenv_length + List.length metasenv; -*) -match subst with - [] -> metasenv - | _ -> - List.map - (fun (n, context, ty) -> - (n, apply_subst_context subst context, apply_subst subst ty)) - (List.filter - (fun (i, _, _) -> not (List.mem_assoc i subst)) - metasenv) - -(***** Pretty printing functions ******) - -let ppterm ~metasenv subst term = - CicPp.ppterm ~metasenv (apply_subst subst term) - -let ppterm_in_name_context ~metasenv subst term name_context = - CicPp.pp ~metasenv (apply_subst subst term) name_context - -let ppterm_in_context ~metasenv subst term context = - let name_context = - List.map (function None -> None | Some (n,_) -> Some n) context - in - ppterm_in_name_context ~metasenv subst term name_context - -let ppterm_in_context_ref = ref ppterm_in_context -let set_ppterm_in_context f = - ppterm_in_context_ref := f -let use_low_level_ppterm_in_context = ref false - -let ppterm_in_context ~metasenv subst term context = - if !use_low_level_ppterm_in_context then - ppterm_in_context ~metasenv subst term context - else - !ppterm_in_context_ref ~metasenv subst term context - -let ppcontext' ~metasenv ?(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_name_context ~metasenv subst t name_context), - (Some n)::name_context - | Some (n,Cic.Def (bo,ty)) -> - sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n) - (ppterm_in_name_context ~metasenv subst ty name_context) - (ppterm_in_name_context ~metasenv subst bo name_context), (Some n)::name_context - | None -> - sprintf "%s_ :? _" (separate i), None::name_context - ) context ("",[]) - -let ppsubst_unfolded ~metasenv subst = - String.concat "\n" - (List.map - (fun (idx, (c, t,ty)) -> - let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in - sprintf "%s |- ?%d : %s := %s" context idx -(ppterm_in_name_context ~metasenv [] ty name_context) - (ppterm_in_name_context ~metasenv subst t name_context)) - subst) -(* - Printf.sprintf "?%d := %s" idx (CicPp.ppterm term)) - subst) *) -;; - -let ppsubst ~metasenv subst = - String.concat "\n" - (List.map - (fun (idx, (c, t, ty)) -> - let context,name_context = ppcontext' ~metasenv ~sep:"; " [] c in - sprintf "%s |- ?%d : %s := %s" context idx (ppterm_in_name_context ~metasenv [] ty name_context) - (ppterm_in_name_context ~metasenv [] t name_context)) - subst) -;; - -let ppcontext ~metasenv ?sep subst context = - fst (ppcontext' ~metasenv ?sep subst context) - -let ppmetasenv ?(sep = "\n") subst metasenv = - String.concat sep - (List.map - (fun (i, c, t) -> - let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in - sprintf "%s |- ?%d: %s" context i - (ppterm_in_name_context ~metasenv subst t name_context)) - (List.filter - (fun (i, _, _) -> not (List.mem_assoc i subst)) - metasenv)) - -let tempi_type_of_aux_subst = ref 0.0;; -let tempi_subst = ref 0.0;; -let tempi_type_of_aux = ref 0.0;; - -(**** DELIFT ****) -(* the delift function takes in input a metavariable index, an ordered list of - * optional terms [t1,...,tn] and a term t, and substitutes every tk = Some - * (rel(nk)) with rel(k). Typically, the list of optional terms is the explicit - * substitution that is applied to a metavariable occurrence and the result of - * the delift function is a term the implicit variable can be substituted with - * to make the term [t] unifiable with the metavariable occurrence. In general, - * the problem is undecidable if we consider equivalence in place of alpha - * convertibility. Our implementation, though, is even weaker than alpha - * convertibility, since it replace the term [tk] if and only if [tk] is a Rel - * (missing all the other cases). Does this matter in practice? - * The metavariable index is the index of the metavariable that must not occur - * in the term (for occur check). - *) - -exception NotInTheList;; - -let position n = - let rec aux k = - function - [] -> raise NotInTheList - | (Some (Cic.Rel m))::_ when m=n -> k - | _::tl -> aux (k+1) tl in - aux 1 +let mk_perforated_irl shift len restrictions = + let rec aux n = + if n = 0 then [] else + if List.mem (n+shift) restrictions then aux (n-1) + else (NCic.Rel n) :: aux (n-1) + in + pack_lc (shift, NCic.Ctx (List.rev (aux len))) ;; exception Occur;; -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 _ - | C.Sort _ as t -> t - | C.Implicit _ -> assert false - | 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) - | C.LetIn (name,so,ty,dest) -> - C.LetIn (name, aux k so, aux k ty, aux (k+1) dest) - | C.Appl l -> C.Appl (List.map (aux k) l) - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst - in - C.Var (uri, exp_named_subst') - | C.Const (uri, exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst - in - C.Const (uri, exp_named_subst') - | C.MutInd (uri,tyno,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst - in - C.MutInd (uri, tyno, exp_named_subst') - | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst +let rec force_does_not_occur metasenv subst restrictions t = + let rec aux k ms = function + | NCic.Rel r when List.mem (r - k) restrictions -> raise Occur + | NCic.Rel r as orig -> + let amount = + List.length (List.filter (fun x -> x < r - k) restrictions) in - C.MutConstruct (uri, tyno, consno, exp_named_subst') - | C.MutCase (uri,tyno,out,te,pl) -> - C.MutCase (uri, tyno, aux k out, aux k te, List.map (aux k) pl) - | C.Fix (i,fl) -> - let len = List.length fl in - let k_plus_len = k + len in - let fl' = - List.map - (fun (name,j,ty,bo) -> (name, j, aux k ty, aux k_plus_len bo)) fl - in - C.Fix (i, fl') - | C.CoFix (i,fl) -> - let len = List.length fl in - let k_plus_len = k + len in - let fl' = - List.map - (fun (name,ty,bo) -> (name, aux k ty, aux k_plus_len bo)) fl + if amount > 0 then ms, NCic.Rel (r - amount) else ms, orig + | NCic.Meta (n, (shift,lc as l)) as orig -> + (* we ignore the subst since restrict will take care of already + * instantiated/restricted metavariabels *) + let (metasenv,subst as ms), restrictions_for_n, l' = + let l = NCicUtils.expand_local_context lc in + + let ms, _, restrictions_for_n, l = + List.fold_right + (fun t (ms, i, restrictions_for_n, l) -> + try + let ms, t = aux (k-shift) ms t in + ms, i-1, restrictions_for_n, t::l + with Occur -> + ms, i-1, i::restrictions_for_n, l) + l (ms, List.length l, [], []) + in + + ms, restrictions_for_n, pack_lc (shift, NCic.Ctx l) in - C.CoFix (i, fl') - in - let res = aux 0 t in - (!more_to_be_restricted, res) - -let rec restrict subst to_be_restricted metasenv = - match to_be_restricted with - | [] -> metasenv, subst - | _ -> - let names_of_context_indexes context indexes = - String.concat ", " - (List.map - (fun i -> - try - match List.nth context (i-1) 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 - | Some (name, Cic.Decl t) -> - 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') - | Some (name, Cic.Def (bo, ty)) -> - let (more_to_be_restricted, bo') = - force_does_not_occur subst to_be_restricted bo - in - let more_to_be_restricted, ty' = - let more_to_be_restricted', ty' = - force_does_not_occur subst to_be_restricted ty + if restrictions_for_n = [] then + ms, if l = l' then orig else NCic.Meta (n, l') + else + let metasenv, subst, newmeta = + restrict metasenv subst n restrictions_for_n in - more_to_be_restricted @ more_to_be_restricted', - ty' - in - more_to_be_restricted, Some (name, Cic.Def (bo', ty')) - in - let rec erase i to_be_restricted n = function - | [] -> [], to_be_restricted, [] - | hd::tl -> - 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 - more_to_be_restricted, restricted, None:: tl' - else - (try - 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' - with Occur -> - more_to_be_restricted, (i :: restricted), None :: tl') - in - let (more_to_be_restricted, metasenv) = (* restrict metasenv *) - List.fold_right - (fun (n, context, t) (more, metasenv) -> - let to_be_restricted = - 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 + (metasenv, subst), NCic.Meta (newmeta, l') + | t -> NCicUntrusted.map_term_fold_a (fun _ k -> k+1) k aux ms t + in + aux 0 (metasenv,subst) t + +and force_does_not_occur_in_context metasenv subst restrictions = function + | name, NCic.Decl t as orig -> + let (metasenv, subst), t' = + force_does_not_occur metasenv subst restrictions t in + metasenv, subst, (if t == t' then orig else (name,NCic.Decl t')) + | name, NCic.Def (bo, ty) as orig -> + let (metasenv, subst), bo' = + force_does_not_occur metasenv subst restrictions bo in + let (metasenv, subst), ty' = + force_does_not_occur metasenv subst restrictions ty in + metasenv, subst, + (if bo == bo' && ty == ty' then orig else (name, NCic.Def (bo', ty'))) + +and erase_in_context metasenv subst pos restrictions = function + | [] -> metasenv, subst, restrictions, [] + | hd::tl as orig -> + let metasenv, subst, restricted, tl' = + erase_in_context metasenv subst (pos+1) restrictions tl in + if List.mem pos restricted then + metasenv, subst, restricted, tl' + else try - let more_to_be_restricted', t' = - force_does_not_occur subst restricted t + let metasenv, subst, hd' = + let delifted_restricted = + List.map ((+) ~-pos) (List.filter ((<=) pos) restricted) in + force_does_not_occur_in_context + metasenv subst delifted_restricted hd in - let metasenv' = (n, context', t') :: metasenv in - (more @ more_to_be_restricted @ more_to_be_restricted', - metasenv') + metasenv, subst, restricted, + (if hd' == hd && tl' == tl then orig else (hd' :: tl')) with Occur -> - raise (MetaSubstFailure (lazy (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 ([], []) - in - let (more_to_be_restricted', subst) = (* restrict subst *) - List.fold_right - (* TODO: cambiare dopo l'aggiunta del ty *) - (fun (n, (context, term,ty)) (more, subst') -> - let to_be_restricted = - List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted) + metasenv, subst, (pos :: restricted), tl' + +and restrict metasenv subst i restrictions = + assert (restrictions <> []); + try + let name, ctx, bo, ty = NCicUtils.lookup_subst i subst in + try + let metasenv, subst, restrictions, newctx = + erase_in_context metasenv subst 1 restrictions ctx in + let (metasenv, subst), newty = + force_does_not_occur metasenv subst restrictions ty in + let (metasenv, subst), newbo = + force_does_not_occur metasenv subst restrictions bo in + let j = newmeta () in + let subst_entry_j = j, (name, newctx, newbo, newty) in + let reloc_irl = mk_perforated_irl 0 (List.length ctx) restrictions in + let subst_entry_i = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in + let new_subst = + subst_entry_j :: List.map + (fun (n,_) as orig -> if i = n then subst_entry_i else orig) subst 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 more_to_be_restricted'', ty' = - force_does_not_occur subst restricted ty in - let subst' = (n, (context', term',ty')) :: subst' in - let more = - more @ more_to_be_restricted - @ more_to_be_restricted'@more_to_be_restricted'' in - (more, subst') - with Occur -> - let error_msg = lazy (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 ~metasenv subst term)) - in - (* DEBUG - debug_print (lazy error_msg); - debug_print (lazy ("metasenv = \n" ^ (ppmetasenv metasenv subst))); - debug_print (lazy ("subst = \n" ^ (ppsubst subst))); - debug_print (lazy ("context = \n" ^ (ppcontext subst context))); *) - raise (MetaSubstFailure error_msg))) - subst ([], []) - in - restrict subst (more_to_be_restricted @ more_to_be_restricted') metasenv +(* + prerr_endline ("restringo nella subst: " ^string_of_int i ^ " -> " ^ + string_of_int j ^ "\n" ^ + NCicPp.ppsubst ~metasenv [subst_entry_j] ^ "\n\n" ^ + NCicPp.ppsubst ~metasenv [subst_entry_i] ^ "\n" ^ + NCicPp.ppterm ~metasenv ~subst ~context:ctx bo ^ " ---- " ^ + NCicPp.ppterm ~metasenv ~subst ~context:newctx newbo + ); +*) + metasenv, new_subst, j + with Occur -> raise (MetaSubstFailure (lazy (Printf.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") i (String.concat ", " + (List.map (fun x -> fst (List.nth ctx (x-1))) restrictions)) i + (NCicPp.ppterm ~metasenv ~subst ~context:ctx bo)))) + with NCicUtils.Subst_not_found _ -> + try + let name, ctx, ty = NCicUtils.lookup_meta i metasenv in + try + let metasenv, subst, restrictions, newctx = + erase_in_context metasenv subst 1 restrictions ctx in + let (metasenv, subst), newty = + force_does_not_occur metasenv subst restrictions ty in + let j = newmeta () in + let metasenv_entry = j, (name, newctx, newty) in + let reloc_irl = + mk_perforated_irl 0 (List.length ctx) restrictions in + let subst_entry = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in + List.map + (fun (n,_) as orig -> if i = n then metasenv_entry else orig) + metasenv, + subst_entry :: subst, j + with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf + ("Cannot restrict the context of the metavariable ?%d "^^ + "over the hypotheses %s since metavariable's type depends "^^ + "on at least one of them") i (String.concat ", " + (List.map (fun x -> fst (List.nth ctx (x-1))) restrictions))))) + with + | NCicUtils.Meta_not_found _ -> assert false ;; -(*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)(*Andrea: maybe not*) +let rec flexible_arg subst = function + | NCic.Meta (i,_) | NCic.Appl (NCic.Meta (i,_) :: _)-> + (try + let _,_,t,_ = List.assoc i subst in + flexible_arg subst t + with Not_found -> true) + | _ -> false +;; -let delift n subst context metasenv l t = -(* INVARIANT: we suppose that t is not another occurrence of Meta(n,_), - otherwise the occur check does not make sense *) +let flexible subst l = List.exists (flexible_arg subst) l;; + +let in_scope_tag = "tag:in_scope" ;; +let out_scope_tag_prefix = "tag:out_scope:" +let out_scope_tag n = out_scope_tag_prefix ^ string_of_int n ;; +let is_out_scope_tag tag = + String.length tag > String.length out_scope_tag_prefix && + String.sub tag 0 (String.length out_scope_tag_prefix) = out_scope_tag_prefix +;; +let int_of_out_scope_tag tag = + int_of_string + (String.sub tag (String.length out_scope_tag_prefix) + (String.length tag - (String.length out_scope_tag_prefix))) +;; -(* - debug_print (lazy ("sto deliftando il termine " ^ (CicPp.ppterm t) ^ " rispetto - al contesto locale " ^ (CicPp.ppterm (Cic.Meta(0,l))))); -*) - let module S = CicSubstitution in - let l = - let (_, canonical_context, _) = - try - CicUtil.lookup_meta n metasenv - with CicUtil.Meta_not_found _ -> - raise (MetaSubstFailure (lazy - ("delifting error: the metavariable " ^ string_of_int n ^ " is not " ^ - "declared in the metasenv"))) +exception Found;; + +(* INVARIANT: we suppose that t is not another occurrence of Meta(n,_), + otherwise the occur check does not make sense in case of unification + of ?n with ?n *) +let delift ~unify metasenv subst context n l t = + let is_in_scope_meta subst = function + | NCic.Meta (i,_) -> + (try + let tag, _, _, _ = NCicUtils.lookup_subst i subst in + tag = Some in_scope_tag + with NCicUtils.Subst_not_found _ -> false) + | _ -> false + in + let contains_in_scope subst t = + let rec aux _ () = function + | NCic.Meta _ as t -> + if is_in_scope_meta subst t then raise Found + else () + | t -> + if is_in_scope_meta subst t then raise Found + else NCicUtils.fold (fun _ () -> ()) () aux () t in - List.map2 (fun ct lt -> - match (ct, lt) with - | None, _ -> None - | Some _, _ -> lt) - canonical_context l + try aux () () t; false with Found -> true in - let to_be_restricted = ref [] in - let rec deliftaux k = - let module C = Cic in - function - | C.Rel m as t-> - if m <=k then - t - else - (try - match List.nth context (m-k-1) with - Some (_,C.Def (t,_)) -> - (try - C.Rel ((position (m-k) l) + k) - with - NotInTheList -> - (*CSC: Hmmm. This bit of reduction is not in the spirit of *) - (*CSC: first order unification. Does it help or does it harm? *) - (*CSC: ANSWER: it hurts performances since it is possible to *) - (*CSC: have an exponential explosion of the size of the proof.*) - (*CSC: However, without this bit of reduction some "apply" in *) - (*CSC: the library fail (e.g. nat/nth_prime.ma). *) - deliftaux k (S.lift m t)) - | Some (_,C.Decl t) -> - C.Rel ((position (m-k) l) + k) - | None -> raise (MetaSubstFailure (lazy "RelToHiddenHypothesis")) - with - Failure _ -> - raise (MetaSubstFailure (lazy "Unbound variable found in deliftaux")) - ) - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst - in - C.Var (uri,exp_named_subst') - | C.Meta (i, l1) as t -> - (try - let (_,t,_) = CicUtil.lookup_subst i subst in - deliftaux k (CicSubstitution.subst_meta l1 t) - with CicUtil.Subst_not_found _ -> - (* see the top level invariant *) - if (i = n) then - raise (MetaSubstFailure (lazy (sprintf - "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)" - i (ppterm ~metasenv subst t)))) - else - begin - (* 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' + let unify_list ~alpha in_scope = + match l with + | _, NCic.Irl _ -> fun _ _ _ _ _ -> None + | shift, NCic.Ctx l -> fun metasenv subst context k t -> + if flexible_arg subst t || contains_in_scope subst t then None else + let lb = List.map (fun t -> t, flexible_arg subst t) l in + HExtlib.list_findopt + (fun (li,flexible) i -> + if flexible || i < in_scope then None else + let li = NCicSubstitution.lift (k+shift) li in + if alpha then + if NCicReduction.alpha_eq metasenv subst context li t then + Some ((metasenv,subst), NCic.Rel (i+1+k)) + else + None + else + match unify metasenv subst context li t with + | Some (metasenv,subst) -> + Some ((metasenv, subst), NCic.Rel (i+1+k)) + | None -> None) + lb + in + let rec aux (context,k,in_scope) (metasenv, subst as ms) t = + match unify_list ~alpha:true in_scope metasenv subst context k t with + | Some x -> x + | None -> + try + match t with + | NCic.Rel n as t when n <= k -> ms, t + | NCic.Rel n -> + (try + match List.nth context (n-k-1) with + | _,NCic.Def (bo,_) -> + (try ms, NCic.Rel ((position in_scope (n-k) l) + k) + with NotInTheList -> + (* CSC: This bit of reduction hurts performances since it is + * possible to have an exponential explosion of the size of the + * proof. required for nat/nth_prime.ma *) + aux (context,k,in_scope) ms (NCicSubstitution.lift n bo)) + | _,NCic.Decl _ -> ms, NCic.Rel ((position in_scope (n-k) l) + k) + with Failure _ -> assert false) (*Unbound variable found in delift*) + | NCic.Meta (i,_) when i=n -> + raise (MetaSubstFailure (lazy (Printf.sprintf ( + "Cannot unify the metavariable ?%d with a term that has "^^ + "as subterm %s in which the same metavariable "^^ + "occurs (occur check)") i + (NCicPp.ppterm ~context ~metasenv ~subst t)))) + | NCic.Meta (i,l1) as orig -> + (try + let tag,c,t,ty = NCicUtils.lookup_subst i subst in + let in_scope, clear = + match tag with + | Some tag when tag = in_scope_tag -> 0, true + | Some tag when is_out_scope_tag tag->int_of_out_scope_tag tag,true + | _ -> in_scope, false + in + let ms = + if not clear then ms + else + metasenv, + (i,(None,c,t,ty)) :: List.filter (fun j,_ -> i <> j) subst + in + aux (context,k,in_scope) ms (NCicSubstitution.subst_meta l1 t) + with NCicUtils.Subst_not_found _ -> + if snd l1 = NCic.Irl 0 || snd l1 = NCic.Ctx [] then ms, orig + else + let shift1,lc1 = l1 in + let shift,lc = l in + let shift = shift + k in + match lc, lc1 with + | NCic.Irl len, NCic.Irl len1 + when shift1 + len1 < shift || shift1 > shift + len -> + let restrictions = HExtlib.list_seq 1 (len1 + 1) in + let metasenv, subst, newmeta = + restrict metasenv subst i restrictions + in + (metasenv, subst), + NCic.Meta (newmeta, (0,NCic.Irl (max 0 (k-shift1)))) + | NCic.Irl len, NCic.Irl len1 -> + let low_restrictions, new_shift = + if k <= shift1 && shift1 < shift then + HExtlib.list_seq 1 (shift - shift1 + 1), k + else if shift1 < k (* <= shift *) then + let save_below = k - shift1 in + HExtlib.list_seq (save_below + 1) (shift - shift1 + 1), + shift1 + else [], shift1 - shift + k + in + let high_restrictions = + let last = shift + len in + let last1 = shift1 + len1 in + if last1 > last then + let high_gap = last1 - last in + HExtlib.list_seq (len1 - high_gap + 1) (len1 + 1) + else [] + in + let restrictions = low_restrictions @ high_restrictions in + if restrictions = [] then + if shift = k then ms, orig + else ms, NCic.Meta (i, (new_shift, lc1)) + else + let metasenv, subst, newmeta = + restrict metasenv subst i restrictions + in +(* {{{ + prerr_endline ("RESTRICTIONS FOR: " ^ + NCicPp.ppterm ~metasenv ~subst ~context:[] + (NCic.Meta (i,l1))^" that was part of a term unified with " + ^ NCicPp.ppterm ~metasenv ~subst ~context:[] (NCic.Meta + (n,l)) ^ " ====> " ^ String.concat "," (List.map + string_of_int restrictions) ^ "\nMENV:\n" ^ + NCicPp.ppmetasenv ~subst metasenv ^ "\nSUBST:\n" ^ + NCicPp.ppsubst subst ~metasenv); +}}} *) + let newlc_len = len1 - List.length restrictions in + let meta = + NCic.Meta(newmeta,(new_shift, NCic.Irl newlc_len)) + in + assert ( + let _, cctx, _ = NCicUtils.lookup_meta newmeta metasenv in + List.length cctx = newlc_len); + (metasenv, subst), meta + + | _ -> + let lc1 = NCicUtils.expand_local_context lc1 in + let lc1 = List.map (NCicSubstitution.lift shift1) lc1 in + let rec deliftl tbr j ms = function + | [] -> ms, tbr, [] + | t::tl -> + let ms, tbr, tl = deliftl tbr (j+1) ms tl in + try + let ms, t = aux (context,k,in_scope) ms t in + ms, tbr, t::tl with - NotInTheList - | MetaSubstFailure _ -> - to_be_restricted := - (i,j)::!to_be_restricted ; None::l1' - in - let l' = deliftl 1 l1 in - C.Meta(i,l') - end) - | C.Sort _ as t -> t - | C.Implicit _ as t -> t - | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty) - | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t) - | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t) - | C.LetIn (n,s,ty,t) -> - C.LetIn (n, deliftaux k s, deliftaux k ty, deliftaux (k+1) t) - | C.Appl l -> C.Appl (List.map (deliftaux k) l) - | C.Const (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst - in - C.Const (uri,exp_named_subst') - | C.MutInd (uri,typeno,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst - in - C.MutInd (uri,typeno,exp_named_subst') - | C.MutConstruct (uri,typeno,consno,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst - in - C.MutConstruct (uri,typeno,consno,exp_named_subst') - | C.MutCase (sp,i,outty,t,pl) -> - C.MutCase (sp, i, deliftaux k outty, deliftaux k t, - List.map (deliftaux k) pl) - | C.Fix (i, fl) -> - let len = List.length fl in - let liftedfl = - List.map - (fun (name, i, ty, bo) -> - (name, i, deliftaux k ty, deliftaux (k+len) bo)) - fl - in - C.Fix (i, liftedfl) - | C.CoFix (i, fl) -> - let len = List.length fl in - let liftedfl = - List.map - (fun (name, ty, bo) -> (name, deliftaux k ty, deliftaux (k+len) bo)) - fl - in - C.CoFix (i, liftedfl) + | NotInTheList | MetaSubstFailure _ -> ms, j::tbr, tl + in + let (metasenv, subst), to_be_r, lc1' = deliftl [] 1 ms lc1 in +(* + prerr_endline ("TO BE RESTRICTED: " ^ + (String.concat "," (List.map string_of_int to_be_r))); +*) + let l1 = pack_lc (0, NCic.Ctx lc1') in +(* + prerr_endline ("newmeta:" ^ NCicPp.ppterm + ~metasenv ~subst ~context (NCic.Meta (999,l1))); +*) + if to_be_r = [] then + (metasenv, subst), + (if lc1' = lc1 then orig else NCic.Meta (i,l1)) + else + let metasenv, subst, newmeta = + restrict metasenv subst i to_be_r in + (metasenv, subst), NCic.Meta(newmeta,l1)) + + | t -> + NCicUntrusted.map_term_fold_a + (fun e (c,k,s) -> (e::c,k+1,s)) (context,k,in_scope) aux ms t + with NotInTheList -> + match unify_list ~alpha:false in_scope metasenv subst context k t with + | Some x -> x + | None -> raise NotInTheList in - let res = - try - deliftaux 0 t - with - NotInTheList -> + try aux (context,0,0) (metasenv,subst) t + with NotInTheList -> (* This is the case where we fail even first order unification. *) (* The reason is that our delift function is weaker than first *) (* order (in the sense of alpha-conversion). See comment above *) (* related to the delift function. *) -(* debug_print (lazy "First Order UnificationFailure during delift") ; -debug_print(lazy (sprintf - "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables" - (ppterm subst t) - (String.concat "; " - (List.map - (function Some t -> ppterm subst t | None -> "_") l - )))); *) - let msg = (lazy (sprintf - "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables" - (ppterm ~metasenv subst t) - (String.concat "; " - (List.map - (function Some t -> ppterm ~metasenv subst t | None -> "_") - l)))) + let msg = (lazy (Printf.sprintf + ("Error trying to abstract %s over [%s]: the algorithm only tried to "^^ + "abstract over bound variables") (NCicPp.ppterm ~metasenv ~subst + ~context t) (String.concat "; " (List.map (NCicPp.ppterm ~metasenv + ~subst ~context) (let shift, lc = l in List.map (NCicSubstitution.lift + shift) (NCicUtils.expand_local_context lc)))))) in + let shift, lc = l in + let lc = NCicUtils.expand_local_context lc in + let l = List.map (NCicSubstitution.lift shift) lc in if - List.exists - (function - Some t -> CicUtil.is_meta_closed (apply_subst subst t) - | None -> true) l + List.exists (fun t-> NCicUntrusted.metas_of_term subst context t = []) l then raise (Uncertain msg) else raise (MetaSubstFailure msg) - in - let (metasenv, subst) = restrict subst !to_be_restricted metasenv in - res, metasenv, subst ;; -(* delifts a term t of n levels strating from k, that is changes (Rel m) - * to (Rel (m - n)) when m > (k + n). if k <= m < k + n delift fails - *) -let delift_rels_from subst metasenv k n = - let rec liftaux subst metasenv k = - let module C = Cic in - function - C.Rel m as t -> - if m < k then - t, subst, metasenv - else if m < k + n then - raise DeliftingARelWouldCaptureAFreeVariable - else - C.Rel (m - n), subst, metasenv - | C.Var (uri,exp_named_subst) -> - let exp_named_subst',subst,metasenv = - List.fold_right - (fun (uri,t) (l,subst,metasenv) -> - let t',subst,metasenv = liftaux subst metasenv k t in - (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv) - in - C.Var (uri,exp_named_subst'),subst,metasenv - | C.Meta (i,l) -> - (try - let (_, t,_) = lookup_subst i subst in - liftaux subst metasenv k (CicSubstitution.subst_meta l t) - with CicUtil.Subst_not_found _ -> - let l',to_be_restricted,subst,metasenv = - let rec aux con l subst metasenv = - match l with - [] -> [],[],subst,metasenv - | he::tl -> - let tl',to_be_restricted,subst,metasenv = - aux (con + 1) tl subst metasenv in - let he',more_to_be_restricted,subst,metasenv = - match he with - None -> None,[],subst,metasenv - | Some t -> - try - let t',subst,metasenv = liftaux subst metasenv k t in - Some t',[],subst,metasenv - with - DeliftingARelWouldCaptureAFreeVariable -> - None,[i,con],subst,metasenv - in - he'::tl',more_to_be_restricted@to_be_restricted,subst,metasenv - in - aux 1 l subst metasenv in - let metasenv,subst = restrict subst to_be_restricted metasenv in - C.Meta(i,l'),subst,metasenv) - | C.Sort _ as t -> t,subst,metasenv - | C.Implicit _ as t -> t,subst,metasenv - | C.Cast (te,ty) -> - let te',subst,metasenv = liftaux subst metasenv k te in - let ty',subst,metasenv = liftaux subst metasenv k ty in - C.Cast (te',ty'),subst,metasenv - | C.Prod (n,s,t) -> - let s',subst,metasenv = liftaux subst metasenv k s in - let t',subst,metasenv = liftaux subst metasenv (k+1) t in - C.Prod (n,s',t'),subst,metasenv - | C.Lambda (n,s,t) -> - let s',subst,metasenv = liftaux subst metasenv k s in - let t',subst,metasenv = liftaux subst metasenv (k+1) t in - C.Lambda (n,s',t'),subst,metasenv - | C.LetIn (n,s,ty,t) -> - let s',subst,metasenv = liftaux subst metasenv k s in - let ty',subst,metasenv = liftaux subst metasenv k ty in - let t',subst,metasenv = liftaux subst metasenv (k+1) t in - C.LetIn (n,s',ty',t'),subst,metasenv - | C.Appl l -> - let l',subst,metasenv = - List.fold_right - (fun t (l,subst,metasenv) -> - let t',subst,metasenv = liftaux subst metasenv k t in - t'::l,subst,metasenv) l ([],subst,metasenv) in - C.Appl l',subst,metasenv - | C.Const (uri,exp_named_subst) -> - let exp_named_subst',subst,metasenv = - List.fold_right - (fun (uri,t) (l,subst,metasenv) -> - let t',subst,metasenv = liftaux subst metasenv k t in - (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv) - in - C.Const (uri,exp_named_subst'),subst,metasenv - | C.MutInd (uri,tyno,exp_named_subst) -> - let exp_named_subst',subst,metasenv = - List.fold_right - (fun (uri,t) (l,subst,metasenv) -> - let t',subst,metasenv = liftaux subst metasenv k t in - (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv) - in - C.MutInd (uri,tyno,exp_named_subst'),subst,metasenv - | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - let exp_named_subst',subst,metasenv = - List.fold_right - (fun (uri,t) (l,subst,metasenv) -> - let t',subst,metasenv = liftaux subst metasenv k t in - (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv) - in - C.MutConstruct (uri,tyno,consno,exp_named_subst'),subst,metasenv - | C.MutCase (sp,i,outty,t,pl) -> - let outty',subst,metasenv = liftaux subst metasenv k outty in - let t',subst,metasenv = liftaux subst metasenv k t in - let pl',subst,metasenv = - List.fold_right - (fun t (l,subst,metasenv) -> - let t',subst,metasenv = liftaux subst metasenv k t in - t'::l,subst,metasenv) pl ([],subst,metasenv) - in - C.MutCase (sp,i,outty',t',pl'),subst,metasenv - | C.Fix (i, fl) -> - let len = List.length fl in - let liftedfl,subst,metasenv = - List.fold_right - (fun (name, i, ty, bo) (l,subst,metasenv) -> - let ty',subst,metasenv = liftaux subst metasenv k ty in - let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in - (name,i,ty',bo')::l,subst,metasenv - ) fl ([],subst,metasenv) - in - C.Fix (i, liftedfl),subst,metasenv - | C.CoFix (i, fl) -> - let len = List.length fl in - let liftedfl,subst,metasenv = - List.fold_right - (fun (name, ty, bo) (l,subst,metasenv) -> - let ty',subst,metasenv = liftaux subst metasenv k ty in - let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in - (name,ty',bo')::l,subst,metasenv - ) fl ([],subst,metasenv) - in - C.CoFix (i, liftedfl),subst,metasenv - in - liftaux subst metasenv k - -let delift_rels subst metasenv n t = - delift_rels_from subst metasenv 1 n t - - -(**** END OF DELIFT ****) - - -(** {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 mk_meta ?name metasenv context ty = + let tyof = function Some s -> Some ("typeof_"^s) | None -> None in + let rec mk_meta name n metasenv context = function + | `WithType ty -> + let len = List.length context in + let menv_entry = (n, (name, context, ty)) in + menv_entry :: metasenv, n, NCic.Meta (n, (0,NCic.Irl len)), ty + | `Sort -> + let ty = NCic.Implicit (`Typeof n) in + mk_meta (tyof name) n metasenv [] (`WithType ty) + | `Type -> + let metasenv, _, ty, _ = + mk_meta (tyof name) (newmeta ()) metasenv context `Sort in + mk_meta name n metasenv context (`WithType ty) + | `Term -> + let metasenv, _, ty, _ = + mk_meta (tyof name) (newmeta ()) metasenv context `Type in + mk_meta name n metasenv context (`WithType ty) + in + mk_meta name (newmeta ()) metasenv context ty +;; -let fppsubst ppf subst = fpp_gen ppf (ppsubst ~metasenv:[] subst) -let fppterm ppf term = fpp_gen ppf (CicPp.ppterm term) -let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv [] metasenv) -*) +let saturate ?(delta=0) metasenv subst context ty goal_arity = + assert (goal_arity >= 0); + let rec aux metasenv = function + | NCic.Prod (name,s,t) as ty -> + let metasenv1, _, arg,_ = + mk_meta ~name:name metasenv context (`WithType s) in + let t, metasenv1, args, pno = + aux metasenv1 (NCicSubstitution.subst arg t) + in + if pno + 1 = goal_arity then + ty, metasenv, [], goal_arity+1 + else + t, metasenv1, arg::args, pno+1 + | ty -> + match NCicReduction.whd ~subst context ty ~delta with + | NCic.Prod _ as ty -> aux metasenv ty + | ty -> ty, metasenv, [], 0 + in + let res, newmetasenv, arguments, _ = aux metasenv ty in + res, newmetasenv, arguments +;;