]> matita.cs.unibo.it Git - helm.git/blob - helm/interface/cicSubstitution.ml
Requires and Provides now fixed
[helm.git] / helm / interface / cicSubstitution.ml
1 let lift n =
2  let rec liftaux k =
3   let module C = Cic in
4    function
5       C.Rel m ->
6        if m < k then
7         C.Rel m
8        else
9         C.Rel (m + n)
10     | C.Var _  as t -> t
11     | C.Meta _ as t -> t
12     | C.Sort _ as t -> t
13     | C.Implicit as t -> t
14     | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty)
15     | C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t)
16     | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t)
17     | C.Appl l -> C.Appl (List.map (liftaux k) l)
18     | C.Const _ as t -> t
19     | C.Abst _  as t -> t
20     | C.MutInd _ as t -> t
21     | C.MutConstruct _ as t -> t
22     | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
23        C.MutCase (sp, cookingsno, i, liftaux k outty, liftaux k t,
24         List.map (liftaux k) pl)
25     | C.Fix (i, fl) ->
26        let len = List.length fl in
27        let liftedfl =
28         List.map
29          (fun (name, i, ty, bo) -> (name, i, liftaux k ty, liftaux (k+len) bo))
30           fl
31        in
32         C.Fix (i, liftedfl)
33     | C.CoFix (i, fl) ->
34        let len = List.length fl in
35        let liftedfl =
36         List.map
37          (fun (name, ty, bo) -> (name, liftaux k ty, liftaux (k+len) bo))
38           fl
39        in
40         C.CoFix (i, liftedfl)
41  in
42   liftaux 1
43 ;;
44
45 let subst arg =
46  let rec substaux k =
47   let module C = Cic in
48    function
49       C.Rel n as t ->
50        (match n with
51            n when n = k -> lift (k - 1) arg
52          | n when n < k -> t
53          | _            -> C.Rel (n - 1)
54        )
55     | C.Var _ as t  -> t
56     | C.Meta _ as t -> t
57     | C.Sort _ as t -> t
58     | C.Implicit as t -> t
59     | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty) (*CSC ??? *)
60     | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
61     | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
62     | C.Appl l -> C.Appl (List.map (substaux k) l)
63     | C.Const _ as t -> t
64     | C.Abst _ as t -> t
65     | C.MutInd _ as t -> t
66     | C.MutConstruct _ as t -> t
67     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
68        C.MutCase (sp,cookingsno,i,substaux k outt, substaux k t,
69         List.map (substaux k) pl)
70     | C.Fix (i,fl) ->
71        let len = List.length fl in
72        let substitutedfl =
73         List.map
74          (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo))
75           fl
76        in
77         C.Fix (i, substitutedfl)
78     | C.CoFix (i,fl) ->
79        let len = List.length fl in
80        let substitutedfl =
81         List.map
82          (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo))
83           fl
84        in
85         C.CoFix (i, substitutedfl)
86  in
87   substaux 1
88 ;;
89
90 let undebrujin_inductive_def uri =
91  function
92     Cic.InductiveDefinition (dl,params,n_ind_params) ->
93      let dl' =
94       List.map
95        (fun (name,inductive,arity,constructors) ->
96          let constructors' =
97           List.map
98            (fun (name,ty,r) ->
99              let ty' =
100               let counter = ref (List.length dl) in
101                List.fold_right
102                 (fun _ ->
103                   decr counter ;
104                   subst (Cic.MutInd (uri,0,!counter))
105                 ) dl ty
106              in
107               (name,ty',r)
108            ) constructors
109          in
110           (name,inductive,arity,constructors')
111        ) dl
112       in
113        Cic.InductiveDefinition (dl', params, n_ind_params)
114   | obj -> obj
115 ;;