* http://cs.unibo.it/helm/.
*)
+exception CannotSubstInMeta;;
+exception RelToHiddenHypothesis;;
+
let lift n =
let rec liftaux k =
let module C = Cic in
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)
| _ -> 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)
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
+;;
projects / helm.git / blobdiff