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