helm/interface/cicCooking.ml

   1 exception Impossible;;
   2 exception NotImplemented of int * string;;
   3 exception WrongUriToConstant;;
   4 exception WrongUriToVariable of string;;
   5 exception WrongUriToInductiveDefinition;;
   6
   7 (* mem x lol is true if x is a member of one    *)
   8 (* of the lists of the list of (int * list) lol *)
   9 let mem x lol =
  10  List.fold_right (fun (_,l) i -> i || List.mem x l) lol false
  11 ;;
  12
  13 (* cook var term *)
  14 let cook curi cookingsno var =
  15  let rec aux k =
  16   let module C = Cic in
  17    function
  18       C.Rel n as t ->
  19        (match n with
  20            n when n >= k -> C.Rel (n + 1)
  21          | _ -> C.Rel n
  22        )
  23     | C.Var uri as t ->
  24        if UriManager.eq uri var then
  25         C.Rel k
  26        else
  27         t
  28     | C.Meta _ as t -> t
  29     | C.Sort _ as t -> t
  30     | C.Implicit as t -> t
  31     | C.Cast (te, ty) -> C.Cast (aux k te, aux k ty)
  32     | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k + 1) t)
  33     | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k + 1) t)
  34     | C.Appl (he::tl) ->
  35        (* Get rid of C.Appl (C.Appl l1) l2 *)
  36        let newtl = List.map (aux k) tl in
  37         (match aux k he with
  38             C.Appl (he'::tl') -> C.Appl (he'::(tl'@newtl))
  39           | t -> C.Appl (t::newtl)
  40         )
  41     | C.Appl [] -> raise Impossible
  42     | C.Const (uri,_) ->
  43        if match CicCache.get_obj uri with
  44            C.Definition (_,_,_,params) when mem var params -> true
  45          | C.Definition _ -> false
  46          | C.Axiom (_,_,params) when mem var params -> true
  47          | C.Axiom _ -> false
  48          | C.CurrentProof _ ->
  49             raise (NotImplemented (2,(UriManager.string_of_uri uri)))
  50          | _ -> raise WrongUriToConstant
  51        then
  52         C.Appl
  53          ((C.Const (uri,UriManager.relative_depth curi uri cookingsno))::
  54           [C.Rel k])
  55        else
  56         C.Const (uri,UriManager.relative_depth curi uri cookingsno)
  57     | C.Abst _ as t -> t
  58     | C.MutInd (uri,_,i) ->
  59        if match CicCache.get_obj uri with
  60            C.InductiveDefinition (_,params,_) when mem var params -> true
  61          | C.InductiveDefinition _ -> false
  62          | _ -> raise WrongUriToInductiveDefinition
  63        then
  64         C.Appl ((C.MutInd (uri,UriManager.relative_depth curi uri cookingsno,i))::[C.Rel k])
  65        else
  66         C.MutInd (uri,UriManager.relative_depth curi uri cookingsno,i)
  67     | C.MutConstruct (uri,_,i,j) ->
  68        if match CicCache.get_obj uri with
  69            C.InductiveDefinition (_,params,_) when mem var params -> true
  70          | C.InductiveDefinition _ -> false
  71          | _ -> raise WrongUriToInductiveDefinition
  72        then
  73         C.Appl ((C.MutConstruct (uri,UriManager.relative_depth curi uri cookingsno,i,j))::[C.Rel k])
  74        else
  75         C.MutConstruct (uri,UriManager.relative_depth curi uri cookingsno,i,j)
  76     | C.MutCase (uri,_,i,outt,term,pl) ->
  77        let substitutedfl =
  78         List.map (aux k) pl
  79        in
  80         C.MutCase (uri,UriManager.relative_depth curi uri cookingsno,i,
  81          aux k outt,aux k term, substitutedfl)
  82     | C.Fix (i,fl) ->
  83        let len = List.length fl in
  84        let substitutedfl =
  85          List.map
  86           (fun (name,i,ty,bo) -> (name,i,aux k ty, aux (k+len) bo))
  87           fl
  88        in
  89         C.Fix (i, substitutedfl)
  90     | C.CoFix (i,fl) ->
  91        let len = List.length fl in
  92        let substitutedfl =
  93          List.map
  94           (fun (name,ty,bo) -> (name,aux k ty, aux (k+len) bo))
  95           fl
  96        in
  97         C.CoFix (i, substitutedfl)
  98  in
  99   aux 1
 100 ;;
 101
 102 let cook_gen add_binder curi cookingsno ty vars =
 103  let module C = Cic in
 104  let module U = UriManager in
 105   let rec cookrec ty =
 106    function
 107      var::tl ->
 108       let (varname, vartype) =
 109        match CicCache.get_obj var with
 110           C.Variable (varname, vartype) -> (varname, vartype)
 111         | _ -> raise (WrongUriToVariable (U.string_of_uri var))
 112       in
 113        cookrec (add_binder (C.Name varname) vartype (cook curi cookingsno var ty)) tl
 114    | _ -> ty
 115   in
 116    cookrec ty vars
 117 ;;
 118
 119 let cook_prod =
 120  cook_gen (fun n s t -> Cic.Prod (n,s,t))
 121 and cook_lambda =
 122  cook_gen (fun n s t -> Cic.Lambda (n,s,t))
 123 ;;
 124
 125 (*CSC: sbagliato da rifare e completare *)
 126 let cook_one_level obj curi cookingsno vars =
 127  let module C = Cic in
 128   match obj with
 129      C.Definition (id,te,ty,params) ->
 130       let ty' = cook_prod curi cookingsno ty vars in
 131       let te' = cook_lambda curi cookingsno te vars in
 132        C.Definition (id,te',ty',params)
 133    | C.Axiom (id,ty,parameters) ->
 134       let ty' = cook_prod curi cookingsno ty vars in
 135        C.Axiom (id,ty',parameters)
 136    | C.Variable _ as obj -> obj
 137    | C.CurrentProof (id,conjs,te,ty) ->
 138       let ty' = cook_prod curi cookingsno ty vars in
 139       let te' = cook_lambda curi cookingsno te vars in
 140        C.CurrentProof (id,conjs,te',ty')
 141    | C.InductiveDefinition (dl, params, n_ind_params) ->
 142       let dl' =
 143        List.map
 144         (fun (name,inductive,arity,constructors) ->
 145           let constructors' =
 146           List.map
 147            (fun (name,ty,r) ->
 148              let r' =
 149               match !r with
 150                  None -> raise Impossible
 151                | Some r -> List.map (fun _ -> false) vars @ r
 152              in
 153              (name,cook_prod curi cookingsno ty vars,ref (Some r'))
 154            ) constructors
 155           in
 156            (name,inductive,cook_prod curi cookingsno arity vars,constructors')
 157         ) dl
 158       in
 159        C.InductiveDefinition (dl', params, n_ind_params + List.length vars)
 160 ;;
 161
 162 let cook_obj obj uri =
 163  let module C = Cic in
 164   let params =
 165    match obj with
 166       C.Definition (_,_,_,params) -> params
 167     | C.Axiom (_,_,params) -> params
 168     | C.Variable _ -> []
 169     | C.CurrentProof _ -> []
 170     | C.InductiveDefinition (_,params,_) -> params
 171   in
 172    let rec cook_all_levels obj =
 173     function
 174        [] -> []
 175      | (n,vars)::tl ->
 176         let cooked_obj = cook_one_level obj uri (n + 1) (List.rev vars) in
 177          (n,cooked_obj)::(cook_all_levels cooked_obj tl)
 178    in
 179     cook_all_levels obj (List.rev params)
 180 ;;
 181
 182 CicCache.cook_obj := cook_obj;;