coq.ml 7.79 KB
Newer Older
charguer's avatar
init  
charguer committed
1 2
open Mytools

POTTIER Francois's avatar
POTTIER Francois committed
3 4 5
(** This file contains facilities for representing Coq expressions. Most of
    the core language is supported. A subset of the top-level declarations
    are supported. *)
charguer's avatar
init  
charguer committed
6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25

(*#########################################################################*)
(* ** Syntax of Coq expressions *)

(** Coq variables and paths *)

type var = string
and vars = var list

and typed_var = var * coq
and typed_vars = typed_var list

and coq_path =
  | Coqp_var of var
  | Coqp_dot of coq_path * string

(** Coq expressions *)

and coq =
  | Coq_var of var
charguer's avatar
charguer committed
26
  | Coq_nat of int
charguer's avatar
init  
charguer committed
27 28 29 30 31 32 33 34 35 36 37
  | Coq_int of int
  | Coq_app of coq * coq 
  | Coq_impl of coq * coq 
  | Coq_lettuple of coqs * coq * coq
  | Coq_forall of typed_var * coq
  | Coq_fun of typed_var * coq
  | Coq_wild 
  | Coq_prop
  | Coq_type
  | Coq_tuple of coqs
  | Coq_record of (var * coq) list 
charguer's avatar
charguer committed
38
  | Coq_tag of string * coq list * string option * coq
charguer's avatar
charguer committed
39
  | Coq_annot of coq * coq
charguer's avatar
charguer committed
40
(* DEPRECATED ; maybe future ?  | Coq_list of coq list *)
charguer's avatar
init  
charguer committed
41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58

and coqs = coq list

(** Toplevel declarations *)

type coqtop =
  | Coqtop_def of typed_var * coq
  | Coqtop_param of typed_var
  | Coqtop_instance of typed_var * bool
  | Coqtop_lemma of typed_var
  | Coqtop_proof of string
  | Coqtop_ind of coqind list
  | Coqtop_record of coqind 
  | Coqtop_label of var * int
  | Coqtop_implicit of var * (var * implicit) list
  | Coqtop_register of string * var * var
  | Coqtop_hint_constructors of vars * var
  | Coqtop_hint_unfold of vars * var
charguer's avatar
charguer committed
59 60 61
  | Coqtop_require of vars
  | Coqtop_import of vars
  | Coqtop_require_import of vars
charguer's avatar
init  
charguer committed
62 63 64 65 66 67 68
  | Coqtop_set_implicit_args 
  | Coqtop_text of string
  | Coqtop_declare_module of var * mod_typ
  | Coqtop_module of var * mod_bindings * mod_cast * mod_def
  | Coqtop_module_type of var * mod_bindings * mod_def
  | Coqtop_module_type_include of var
  | Coqtop_end of var
charguer's avatar
charguer committed
69 70
  | Coqtop_custom of string

charguer's avatar
init  
charguer committed
71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99
and coqtops = coqtop list

(** Modules and signatures *)

and mod_cast =
   | Mod_cast_exact of mod_typ
   | Mod_cast_super of mod_typ
   | Mod_cast_free

and mod_def =
   | Mod_def_inline of mod_expr
   | Mod_def_declare

and mod_typ =
   | Mod_typ_var of var
   | Mod_typ_app of vars
   | Mod_typ_with_def of mod_typ * var * coq
   | Mod_typ_with_mod of mod_typ * var * var

and mod_expr = vars

and mod_binding = vars * mod_typ

and mod_bindings = mod_binding list

(** Inductive definitions *)

and coqind = {
   coqind_name : var;
charguer's avatar
charguer committed
100
   coqind_constructor_name : var;
charguer's avatar
init  
charguer committed
101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118
   coqind_targs : typed_vars;
   coqind_ret : coq;
   coqind_branches : typed_vars; }

(** Implicit Arguements declarations *)

and implicit =
  | Coqi_maximal
  | Coqi_implicit
  | Coqi_explicit


(*#########################################################################*)
(* ** Helper functions to construct expressions *)

(** Several Coq constants *)

let coq_false =  
charguer's avatar
charguer committed
119
  Coq_var "Coq.Init.Logic.False"
charguer's avatar
init  
charguer committed
120 121
  
let coq_true =  
charguer's avatar
charguer committed
122
  Coq_var "Coq.Init.Logic.True"
charguer's avatar
init  
charguer committed
123 124

let coq_bool_false =  
charguer's avatar
charguer committed
125
  Coq_var "Coq.Init.Datatypes.false"
charguer's avatar
init  
charguer committed
126 127
  
let coq_bool_true =  
charguer's avatar
charguer committed
128
  Coq_var "Coq.Init.Datatypes.true"
charguer's avatar
init  
charguer committed
129 130

let coq_tt =
charguer's avatar
charguer committed
131
  Coq_var "Coq.Init.Datatypes.tt"
charguer's avatar
init  
charguer committed
132 133

let coq_unit =
charguer's avatar
charguer committed
134
  Coq_var "Coq.Init.Datatypes.unit"
charguer's avatar
init  
charguer committed
135 136

let coq_int =
charguer's avatar
charguer committed
137
  Coq_var "Coq.ZArith.BinInt.Z" 
charguer's avatar
init  
charguer committed
138

charguer's avatar
charguer committed
139 140
let coq_nat =
  Coq_var "Coq.Init.Datatypes.nat"
charguer's avatar
charguer committed
141

charguer's avatar
init  
charguer committed
142
let coq_bool =
charguer's avatar
charguer committed
143
  Coq_var "Coq.Init.Datatypes.bool"
charguer's avatar
init  
charguer committed
144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230

(** Identifier [x] *)

let coq_var x =
  Coq_var x

(** Identifier [@x] *)

let coq_var_at x =
  coq_var ("@" ^ x)

(** List of identifiers [x1 x2 .. xn] *)

let coq_vars xs =
  List.map coq_var xs

(** List of names [(A1:Type)::(A2::Type)::...::(AN:Type)::nil] *)

let coq_types names =
   List.map (fun n -> (n, Coq_type)) names

(** Application to a list of arguments [c e1 e2 .. eN] *)

let coq_apps c args = 
  List.fold_left (fun acc ci -> Coq_app (acc, ci)) c args

(** Application to wildcards [c _ _ .. _] *)

let coq_app_wilds c n =
   coq_apps c (list_make n Coq_wild) 

(** Applications of an identifier to wildcars [x _ _ .. _] *)

let coq_app_var_wilds x n =
   if n = 0 then Coq_var x else coq_app_wilds (coq_var_at x) n

(** Function [fun (x1:T1) .. (xn:Tn) => c] *)

let coq_funs args c =
  List.fold_right (fun ci acc -> Coq_fun (ci, acc)) args c

(** Function [fun (x1:Type) .. (xn:Type) => c] *)

let coq_fun_types names c =
  coq_funs (coq_types names) c

(** Let binding [let (x:T) := t1 in t2] *)

let coq_foralls args c =
  List.fold_right (fun ci acc -> Coq_forall (ci, acc)) args c

(** Universal [forall (x1:T1) .. (xn:Tn), c] *)

let coq_foralls args c =
  List.fold_right (fun ci acc -> Coq_forall (ci, acc)) args c

(** Universal [forall (x1:Type) .. (xn:Type), c] *)

let coq_forall_types names c =
  coq_foralls (coq_types names) c

(** Universal [forall (x1:_) .. (xn:_), c] *)

let coq_foralls_wild names c =
  coq_foralls (List.map (fun n -> (n, Coq_wild)) names) c

(** Implication [c1 -> c2 -> .. -> cn -> c] *)

let coq_impls cs c =
  List.fold_right (fun ci acc -> Coq_impl (ci, acc)) cs c

(** Implication [Type -> Type -> .. -> Type] *)

let coq_impl_types n = 
   coq_impls (list_make n Coq_type) Coq_type

(** Predicate type [A->Prop] *)

let coq_pred c =
  Coq_impl (c, Coq_prop)

(** Product type [(c1 * c2 * .. * cN)%type] *)

let coq_prod cs =
  match cs with 
  | [] -> coq_unit
  | [c] -> c
charguer's avatar
charguer committed
231
  | c0::cs' -> List.fold_left (fun acc c -> coq_apps (Coq_var "Coq.Init.Datatypes.prod") [acc;c]) c0 cs'
charguer's avatar
init  
charguer committed
232

charguer's avatar
charguer committed
233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250
(** List [c1 :: c2 :: .. :: cN] *)

let coq_list xs =
   let ccons = Coq_var (Renaming.get_builtin_constructor "::") in
   let cnil = Coq_var (Renaming.get_builtin_constructor "[]") in
   List.fold_right (fun arg acc -> 
      coq_apps ccons [arg; acc]) xs cnil
   (* DEPRECATED ; maybe future ?
   let coq_list xs =
     Coq_list xs
   *)
   (* DEPRECATED
   let ccons = get_builtin_constructor "::" in
   let cnil = get_builtin_constructor "[]" in
   let cnil = "Coq.Lists.List.nil" in
   let ccons = "Coq.Lists.List.cons" in
   *)

charguer's avatar
init  
charguer committed
251 252 253
(** Logic combinators *)

let coq_eq c1 c2 =
charguer's avatar
charguer committed
254
  coq_apps (Coq_var "Coq.Init.Logic.eq") [ c1; c2 ]
charguer's avatar
init  
charguer committed
255 256

let coq_neq c1 c2 =
charguer's avatar
charguer committed
257
  coq_apps (Coq_var "Coq.Init.Logic.not") [coq_eq c1 c2]
charguer's avatar
init  
charguer committed
258 259

let coq_disj c1 c2 = 
charguer's avatar
charguer committed
260
  coq_apps (Coq_var "Coq.Init.Logic.or") [c1; c2]
charguer's avatar
init  
charguer committed
261 262

let coq_conj c1 c2 = 
charguer's avatar
charguer committed
263
  coq_apps (Coq_var "Coq.Init.Logic.and") [c1; c2]
charguer's avatar
init  
charguer committed
264 265

let coq_neg c =
charguer's avatar
charguer committed
266
  Coq_app (Coq_var "TLC.LibBool.neg", c)
charguer's avatar
init  
charguer committed
267 268

let coq_exist x c1 c2 = 
charguer's avatar
charguer committed
269
  coq_apps (Coq_var "Coq.Init.Logic.ex") [Coq_fun ((x, c1), c2)]
charguer's avatar
init  
charguer committed
270 271 272 273 274 275 276 277 278 279 280 281 282 283

(** Iterated logic combinators *)

let coq_conjs cs =
  match List.rev cs with
  | [] -> Coq_var "true"
  | c::cs -> List.fold_left (fun acc ci -> coq_conj ci acc) c cs

let coq_exists xcs c2 = 
  List.fold_right (fun (x,c) acc -> coq_exist x c acc) xcs c2

(** Arithmetic operations *)

let coq_le c1 c2 =
charguer's avatar
charguer committed
284
  coq_apps (Coq_var "TLC.LibOrder.le") [ c1; c2 ]
charguer's avatar
init  
charguer committed
285

charguer's avatar
charguer committed
286 287 288 289 290 291
let coq_ge c1 c2 =
  coq_apps (Coq_var "TLC.LibOrder.ge") [ c1; c2 ]

let coq_lt c1 c2 =
  coq_apps (Coq_var "TLC.LibOrder.lt") [ c1; c2 ]

charguer's avatar
init  
charguer committed
292
let coq_gt c1 c2 =
charguer's avatar
charguer committed
293
  coq_apps (Coq_var "TLC.LibOrder.gt") [ c1; c2 ]
charguer's avatar
init  
charguer committed
294 295

let coq_plus c1 c2 =
296
  coq_apps (Coq_var "Coq.ZArith.BinInt.Zplus") [ c1; c2 ]
charguer's avatar
init  
charguer committed
297

charguer's avatar
charguer committed
298 299
let coq_minus c1 c2 =
  coq_apps (Coq_var "Coq.ZArith.BinInt.Zminus") [ c1; c2 ]
charguer's avatar
init  
charguer committed
300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330

(** Toplevel *)

let coqtop_def_untyped x c =
   Coqtop_def ((x,Coq_wild), c)

let coqtop_noimplicit x =
   Coqtop_implicit (x,[])

let coqtop_register db x v =
   Coqtop_register (db, x, v)


(*#########################################################################*)
(* ** Representation of labels (notation of the form "'x" := `1`0`1`0) *)

(** --todo: deprecated *)

type label = string

let var_bits_of_int n =
   let rec repr n = 
     if n < 2 then [] else (1+(n mod 2))::(repr (n/2)) in
   List.rev (0::(repr n)) 

let string_of_var_bits vb =
  show_listp (fun b -> string_of_int b) "`" vb

let value_variable n =
  string_of_var_bits (var_bits_of_int n)

charguer's avatar
charguer committed
331 332 333
let coq_tag (tag : string) ?args ?label (term : coq) =
   let args = match args with | None -> [] | Some args -> args in
   Coq_tag ("CFML.CFPrint." ^ tag, args, label, term)
charguer's avatar
init  
charguer committed
334

charguer's avatar
charguer committed
335 336 337
let coq_annot (term : coq) (term_type : coq)  =
   Coq_annot (term, term_type)