From: Claudio Sacerdoti Coen Date: Wed, 22 May 2002 10:09:21 +0000 (+0000) Subject: delift moved from cicSubstitution to cicUnification X-Git-Tag: V_0_3_0_debian_8~86 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=0328c0e2938ce714d5d7358afdca00195577198e delift moved from cicSubstitution to cicUnification --- diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml index 68276d74b..ae51f3580 100644 --- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml @@ -233,105 +233,3 @@ let lift_meta l t = in aux 0 t ;; - -(************************************************************************) -(*CSC: spostare in cic_unification *) - -(* the delift function takes in input an ordered list of integers [n1,...,nk] - and a term t, and relocates rel(nk) to k. Typically, the list of integers - is a parameter of a metavariable occurrence. *) - -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 restrict to_be_restricted = - let rec erase i n = - function - [] -> [] - | _::tl when List.mem (n,i) to_be_restricted -> - None::(erase (i+1) n tl) - | he::tl -> he::(erase (i+1) n tl) in - let rec aux = - function - [] -> [] - | (n,context,t)::tl -> (n,erase 1 n context,t)::(aux tl) in - aux -;; - - -let delift context metasenv l t = - let to_be_restricted = ref [] in - let rec deliftaux k = - let module C = Cic in - function - C.Rel m -> - if m <=k then - C.Rel m (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *) - (*CSC: deliftato la regola per il LetIn *) - else - (match List.nth context (m-k-1) with - Some (_,C.Def t) -> deliftaux k (lift m t) - | Some (_,C.Decl t) -> - (* It may augment to_be_restricted *) - ignore (deliftaux k (lift m t)) ; - C.Rel ((position (m-k) l) + k) - | None -> raise RelToHiddenHypothesis) - | C.Var _ as t -> t - | C.Meta (i, l1) as t -> - 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 - RelToHiddenHypothesis - | NotInTheList -> - 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) - | 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,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t) - | C.Appl l -> C.Appl (List.map (deliftaux k) l) - | C.Const _ as t -> t - | C.Abst _ as t -> t - | C.MutInd _ as t -> t - | C.MutConstruct _ as t -> t - | C.MutCase (sp,cookingsno,i,outty,t,pl) -> - C.MutCase (sp, cookingsno, 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) - in - let res = deliftaux 0 t in - res, restrict !to_be_restricted metasenv -;; diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.mli b/helm/ocaml/cic_proof_checking/cicSubstitution.mli index 641d36fee..8915b814a 100644 --- a/helm/ocaml/cic_proof_checking/cicSubstitution.mli +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.mli @@ -26,6 +26,4 @@ val lift : int -> Cic.term -> Cic.term val subst : Cic.term -> Cic.term -> Cic.term val lift_meta : (Cic.term option) list -> Cic.term -> Cic.term -val delift : - Cic.context -> Cic.metasenv -> (Cic.term option) list -> Cic.term -> Cic.term * Cic.metasenv val undebrujin_inductive_def : UriManager.uri -> Cic.obj -> Cic.obj diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 2f27bea85..4a2cb2430 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -29,6 +29,111 @@ exception OccurCheck;; exception RelToHiddenHypothesis;; exception OpenTerm;; +(**** DELIFT ****) + +(* the delift function takes in input an ordered list of integers [n1,...,nk] + and a term t, and relocates rel(nk) to k. Typically, the list of integers + is a parameter of a metavariable occurrence. *) + +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 restrict to_be_restricted = + let rec erase i n = + function + [] -> [] + | _::tl when List.mem (n,i) to_be_restricted -> + None::(erase (i+1) n tl) + | he::tl -> he::(erase (i+1) n tl) in + let rec aux = + function + [] -> [] + | (n,context,t)::tl -> (n,erase 1 n context,t)::(aux tl) in + aux +;; + + +let delift context metasenv l t = + let module S = CicSubstitution in + let to_be_restricted = ref [] in + let rec deliftaux k = + let module C = Cic in + function + C.Rel m -> + if m <=k then + C.Rel m (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *) + (*CSC: deliftato la regola per il LetIn *) + else + (match List.nth context (m-k-1) with + Some (_,C.Def t) -> deliftaux k (S.lift m t) + | Some (_,C.Decl t) -> + (* It may augment to_be_restricted *) + ignore (deliftaux k (S.lift m t)) ; + C.Rel ((position (m-k) l) + k) + | None -> raise RelToHiddenHypothesis) + | C.Var _ as t -> t + | C.Meta (i, l1) as t -> + 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 + RelToHiddenHypothesis + | NotInTheList -> + 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) + | 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,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t) + | C.Appl l -> C.Appl (List.map (deliftaux k) l) + | C.Const _ as t -> t + | C.Abst _ as t -> t + | C.MutInd _ as t -> t + | C.MutConstruct _ as t -> t + | C.MutCase (sp,cookingsno,i,outty,t,pl) -> + C.MutCase (sp, cookingsno, 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) + in + let res = deliftaux 0 t in + res, restrict !to_be_restricted metasenv +;; + +(**** END OF DELIFT ****) + type substitution = (int * Cic.term) list (* NUOVA UNIFICAZIONE *) @@ -76,7 +181,7 @@ let fo_unif_new metasenv context t1 t2 = prerr_endline ("DELIFT2(" ^ CicPp.ppterm t ^ ")") ; flush stderr ; List.iter (function (Some t) -> prerr_endline ("l: " ^ CicPp.ppterm t) | None -> prerr_endline " _ ") l ; flush stderr ; prerr_endline " let = - S.delift canonical_context metasenv ? t + delift canonical_context metasenv ? t ) canonical_context CSCSCS @@ -287,7 +392,7 @@ let unwind metasenv subst unwinded t = prerr_endline ("DELIFT(" ^ CicPp.ppterm t' ^ ")") ; flush stderr ; List.iter (function (Some t) -> prerr_endline ("l: " ^ CicPp.ppterm t) | None -> prerr_endline " _ ") l ; flush stderr ; prerr_endline " Cic.metasenv -> (Cic.term option) list -> Cic.term -> Cic.term * Cic.metasenv + (* The entry (i,t) in a substitution means that *) (* (META i) have been instantiated with t. *) type substitution = (int * Cic.term) list