X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicSubstitution.ml;h=68276d74bac39f9a68b34cc5349c463908eae610;hb=37f08b2aba9f17d9d609ca0f57d607f437a3d3fc;hp=b683dd258389f93b698403ac801b787354da9a46;hpb=a61f397a3ea3acaf95a04a2aafbf1d3f223a2755;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml index b683dd258..68276d74b 100644 --- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml @@ -23,6 +23,9 @@ * http://cs.unibo.it/helm/. *) +exception CannotSubstInMeta;; +exception RelToHiddenHypothesis;; + let lift n = let rec liftaux k = let module C = Cic in @@ -33,7 +36,15 @@ let lift n = else C.Rel (m + n) | C.Var _ as t -> t - | C.Meta _ as t -> t + | C.Meta (i,l) -> + let l' = + List.map + (function + None -> None + | Some t -> Some (liftaux k t) + ) l + in + C.Meta(i,l') | C.Sort _ as t -> t | C.Implicit as t -> t | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty) @@ -82,7 +93,15 @@ let subst arg = | _ -> C.Rel (n - 1) ) | C.Var _ as t -> t - | C.Meta _ as t -> t + | C.Meta (i, l) as t -> + let l' = + List.map + (function + None -> None + | Some t -> Some (substaux k t) + ) l + in + C.Meta(i,l') | C.Sort _ as t -> t | C.Implicit as t -> t | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty) @@ -151,3 +170,168 @@ let undebrujin_inductive_def uri = Cic.InductiveDefinition (dl', params, n_ind_params) | obj -> obj ;; + +(* l is the relocation list *) + +let lift_meta l t = + let module C = Cic in + if l = [] then t else + let rec aux k = function + C.Rel n as t -> + if n <= k then t else + (try + match List.nth l (n-k-1) with + None -> raise RelToHiddenHypothesis + | Some t -> lift k t + with + (Failure _) -> assert false + ) + | C.Var _ as t -> t + | C.Meta (i,l) -> + let l' = + List.map + (function + None -> None + | Some t -> + try + Some (aux k t) + with + RelToHiddenHypothesis -> None + ) l + in + C.Meta(i,l') + | C.Sort _ as t -> t + | C.Implicit as t -> t + | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) (*CSC ??? *) + | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k + 1) t) + | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k + 1) t) + | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k + 1) t) + | C.Appl l -> C.Appl (List.map (aux 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,outt,t,pl) -> + C.MutCase (sp,cookingsno,i,aux k outt, aux k t, + List.map (aux k) pl) + | C.Fix (i,fl) -> + let len = List.length fl in + let substitutedfl = + List.map + (fun (name,i,ty,bo) -> (name, i, aux k ty, aux (k+len) bo)) + fl + in + C.Fix (i, substitutedfl) + | C.CoFix (i,fl) -> + let len = List.length fl in + let substitutedfl = + List.map + (fun (name,ty,bo) -> (name, aux k ty, aux (k+len) bo)) + fl + in + C.CoFix (i, substitutedfl) + 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 +;;