- (* FIXED: should be ok even if not touched *)
- (* used to hash cons uris on restore to grant URI structure unicity *)
- let restore_uris =
- let module C = Cic in
- let recons uri =
- UriManager.uri_of_string (UriManager.string_of_uri uri)
- in
- let rec restore_in_term =
- function
- (C.Rel _) as t -> t
- | C.Var (uri,exp_named_subst) ->
- let uri' = recons uri in
- let exp_named_subst' =
- List.map
- (function (uri,t) ->(recons uri,restore_in_term t))
- exp_named_subst
- in
- C.Var (uri',exp_named_subst')
- | C.Meta (i,l) ->
- let l' =
- List.map
- (function
- None -> None
- | Some t -> Some (restore_in_term t)
- ) l
- in
- C.Meta(i,l')
- | C.Sort (C.Type u) ->
- CicUniv.assert_univ u;
- C.Sort (C.Type (CicUniv.recons_univ u))
- | C.Sort _ as t -> t
- | C.Implicit _ as t -> t
- | C.Cast (te,ty) -> C.Cast (restore_in_term te, restore_in_term ty)
- | C.Prod (n,s,t) -> C.Prod (n, restore_in_term s, restore_in_term t)
- | C.Lambda (n,s,t) -> C.Lambda (n, restore_in_term s, restore_in_term t)
- | C.LetIn (n,s,t) -> C.LetIn (n, restore_in_term s, restore_in_term t)
- | C.Appl l -> C.Appl (List.map restore_in_term l)
- | C.Const (uri,exp_named_subst) ->
- let uri' = recons uri in
- let exp_named_subst' =
- List.map
- (function (uri,t) -> (recons uri,restore_in_term t)) exp_named_subst
- in
- C.Const (uri',exp_named_subst')
- | C.MutInd (uri,tyno,exp_named_subst) ->
- let uri' = recons uri in
- let exp_named_subst' =
- List.map
- (function (uri,t) -> (recons uri,restore_in_term t)) exp_named_subst
- in
- C.MutInd (uri',tyno,exp_named_subst')
- | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
- let uri' = recons uri in
- let exp_named_subst' =
- List.map
- (function (uri,t) -> (recons uri,restore_in_term t)) exp_named_subst
- in
- C.MutConstruct (uri',tyno,consno,exp_named_subst')
- | C.MutCase (uri,i,outty,t,pl) ->
- C.MutCase (recons uri, i, restore_in_term outty, restore_in_term t,
- List.map restore_in_term pl)
- | C.Fix (i, fl) ->
- let len = List.length fl in
- let liftedfl =
- List.map
- (fun (name, i, ty, bo) ->
- (name, i, restore_in_term ty, restore_in_term 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, restore_in_term ty, restore_in_term bo))
- fl
- in
- C.CoFix (i, liftedfl)
- in
- function
- C.Constant (name,bo,ty,params,attrs) ->
- let bo' =
- match bo with
- None -> None
- | Some bo -> Some (restore_in_term bo)
- in
- let ty' = restore_in_term ty in
- let params' = List.map recons params in
- C.Constant (name, bo', ty', params',attrs)
- | C.CurrentProof (name,conjs,bo,ty,params,attrs) ->
- let conjs' =
- List.map
- (function (i,hyps,ty) ->
- (i,
- List.map (function
- None -> None
- | Some (name,C.Decl t) ->
- Some (name,C.Decl (restore_in_term t))
- | Some (name,C.Def (bo,ty)) ->
- let ty' =
- match ty with
- None -> None
- | Some ty'' -> Some (restore_in_term ty'')
- in
- Some (name,C.Def (restore_in_term bo, ty'))) hyps,
- restore_in_term ty))
- conjs
- in
- let bo' = restore_in_term bo in
- let ty' = restore_in_term ty in
- let params' = List.map recons params in
- C.CurrentProof (name, conjs', bo', ty', params',attrs)
- | C.Variable (name,bo,ty,params,attrs) ->
- let bo' =
- match bo with
- None -> None
- | Some bo -> Some (restore_in_term bo)
- in
- let ty' = restore_in_term ty in
- let params' = List.map recons params in
- C.Variable (name, bo', ty', params',attrs)
- | C.InductiveDefinition (tl,params,paramsno,attrs) ->
- let params' = List.map recons params in
- let tl' =
- List.map (function (name, inductive, ty, constructors) ->
- name,
- inductive,
- restore_in_term ty,
- (List.map
- (function (name, ty) -> name, restore_in_term ty)
- constructors))
- tl
- in
- C.InductiveDefinition (tl', params', paramsno, attrs)
- ;;
-