characteristic.ml 70 KB
Newer Older
charguer's avatar
charguer committed
1 2 3 4 5 6 7 8 9 10 11
open Misc
open Asttypes
open Types
open Typedtree
open Mytools
open Longident
open Print_tast
open Print_type
open Formula
open Coq
open Path
charguer's avatar
charguer committed
12
open Renaming
charguer's avatar
charguer committed
13 14
open Printf

charguer's avatar
charguer committed
15

charguer's avatar
charguer committed
16 17 18 19 20 21 22
(*#########################################################################*)
(* ** Aux *)

(** [list_is_included l1 l2] returns true if any item in [l1] also belongs to [l2] *)

let list_is_included l1 l2 =
   List.for_all (fun x -> List.mem x l2) l1
charguer's avatar
charguer committed
23

charguer's avatar
charguer committed
24

charguer's avatar
charguer committed
25 26 27
(*#########################################################################*)
(* ** Error messages *)

charguer's avatar
charguer committed
28
exception Not_in_normal_form of Location.t * string
charguer's avatar
charguer committed
29

charguer's avatar
charguer committed
30 31
let not_in_normal_form loc s =
   raise (Not_in_normal_form (loc, s))
charguer's avatar
charguer committed
32 33


charguer's avatar
charguer committed
34 35 36 37 38 39
(*#########################################################################*)
(* ** List of external modules that need to be required *)

let external_modules = ref []

let external_modules_add name =
40
   if not (List.mem name !external_modules)
41 42
     then external_modules := name::!external_modules
   (* TODO: use a structure more efficient than lists *)
charguer's avatar
charguer committed
43

44
let external_modules_get_coqtop () =
charguer's avatar
charguer committed
45
   List.map (fun name -> Coqtop_require [name]) !external_modules
charguer's avatar
charguer committed
46

47
let external_modules_reset () =
charguer's avatar
charguer committed
48 49 50
   external_modules := []


charguer's avatar
charguer committed
51

charguer's avatar
charguer committed
52 53 54
(*#########################################################################*)
(* ** Lifting of paths *)

charguer's avatar
charguer committed
55
(* Take a module name and add "_ml" suffix to it;
56
   Moreover, insert a "Require" directive in case the module
charguer's avatar
charguer committed
57
   corresponds to a file (i.e. a compilation unit. *)
charguer's avatar
charguer committed
58

charguer's avatar
charguer committed
59
let lift_module_name id =
charguer's avatar
charguer committed
60
   let name = Ident.name id in
charguer's avatar
charguer committed
61
   let coqname = module_name name in
charguer's avatar
charguer committed
62 63
   if Ident.persistent id then external_modules_add coqname;
   coqname
charguer's avatar
charguer committed
64

charguer's avatar
charguer committed
65
   (* -- old:
66
     if Ident.persistent id
charguer's avatar
charguer committed
67
      then (let result = name ^ "_ml" in external_modules_add result; result)
charguer's avatar
charguer committed
68
      else "ML" ^ name
charguer's avatar
charguer committed
69 70
   *)
   (* -- old: if name = "OkaStream" then "CFPrim" else  *)
charguer's avatar
charguer committed
71

72
(* Function for adding "_ml" to the modules in a path,
charguer's avatar
charguer committed
73 74
   including the last constant which is assumed to a module name.
   For example, "Foo.Bar" becomes "Foo_ml.Bar_ml".
75

charguer's avatar
charguer committed
76 77
   TODO: rename this function *)

charguer's avatar
charguer committed
78

charguer's avatar
charguer committed
79
let rec lift_full_path = function
charguer's avatar
charguer committed
80
  | Pident id -> Pident (Ident.create (lift_module_name id))
81 82
  | Pdot(p, s, pos) -> Pdot(lift_full_path p, (module_name s), pos)
  | Papply(p1, p2) -> assert false
charguer's avatar
charguer committed
83

84
(* Function for adding "_ml" to the modules in a path,
charguer's avatar
charguer committed
85 86
   but not changing the last constant in the path.
   For example, "Foo.x" becomes "Foo_ml.x". *)
charguer's avatar
charguer committed
87

charguer's avatar
charguer committed
88 89
let lift_path = function
  | Pident id -> Pident id
90 91
  | Pdot(p, s, pos) -> Pdot(lift_full_path p, s, pos)
  | Papply(p1, p2) -> assert false
charguer's avatar
charguer committed
92

93
(** Translates a path into a string. A module called "Test"
charguer's avatar
charguer committed
94
    becomes "Test_ml". *)
charguer's avatar
charguer committed
95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116

let lift_full_path_name p =
  Path.name (lift_full_path p)

(** Translates a path into a string --todo: why not full? *)

let lift_path_name p =
  Path.name (lift_path p)


(*#########################################################################*)
(* ** Lifting of types *)

(** Computes the free variables of a [btyp] *)

let rec fv_btyp ?(through_arrow = true) t =
   let aux = fv_btyp in
   match t with
   | Btyp_val -> []
   | Btyp_arrow (t1,t2) -> if through_arrow then aux t1 @ aux t2 else []
   | Btyp_constr (id,ts) -> list_concat_map aux ts
   | Btyp_tuple ts -> list_concat_map aux ts
charguer's avatar
charguer committed
117
   | Btyp_var (s,ty) -> typvar_mark_used ty; [s]
charguer's avatar
charguer committed
118
   | Btyp_poly (ss,t) -> unsupported_noloc "poly-types"
119
   | Btyp_alias (t,s) -> s :: aux t
charguer's avatar
charguer committed
120 121 122

(** Translates a [btyp] into a Coq type *)

charguer's avatar
charguer committed
123 124
let rec lift_btyp loc t =
   let aux = lift_btyp loc in
charguer's avatar
charguer committed
125
   match t with
126
   | Btyp_val ->
charguer's avatar
charguer committed
127
      func_type
128
   | Btyp_arrow (t1,t2) ->
charguer's avatar
charguer committed
129 130
      func_type
   (* DEPRECATED
131
   | Btyp_constr (id,[t]) when Path.name id = "array" ->
charguer's avatar
charguer committed
132
      loc_type *)
133
   | Btyp_constr (id,ts) ->
charguer's avatar
charguer committed
134
      coq_apps (Coq_var (type_constr_name (lift_path_name id))) (List.map aux ts)
135
   | Btyp_tuple ts ->
charguer's avatar
charguer committed
136
      coq_prod (List.map aux ts)
137
   | Btyp_var (s,ty) ->
charguer's avatar
charguer committed
138
      typvar_mark_used ty;
charguer's avatar
charguer committed
139
      Coq_var s
charguer's avatar
charguer committed
140 141 142
      (* DEPRECATED
      if b then unsupported loc ("non-generalizable free type variables (of the form '_a); please add a type annotation if the type is not polymorphic; if it is, then ask to get the typechecker patched for propagating the annotation. var=" ^ s);
       let s = if b then "__" ^ s else s in *)
143
   | Btyp_poly (ss,t) ->
charguer's avatar
charguer committed
144
      unsupported_noloc "poly-types"
145
   | Btyp_alias (t1,s) ->
charguer's avatar
charguer committed
146
      let occ = fv_btyp ~through_arrow:false t1 in
147
      if List.mem s occ
charguer's avatar
charguer committed
148
        then unsupported_noloc ("found a recursive type that is not erased by an arrow:" ^ (print_out_type t));
149
      aux t1
charguer's avatar
charguer committed
150

charguer's avatar
charguer committed
151 152 153 154 155 156 157 158
(* TEMPORARILY DEPRECATED

   | Btyp_constr (id,[t]) when Path.name id = "ref" || Path.name id = "Pervasives.ref" ->
      loc_type

   | Btyp_constr (id,[t]) when Path.name id = "heap" || Path.name id = "Heap.heap" ->
      loc_type

159 160 161
   | Btyp_constr (id,[t]) when Path.same id Predef.path_lazy_t || Path.name id = "Lazy.t" ->
      aux t
   | Btyp_constr (id,[t]) when Path.name id = "Stream.stream" || Path.name id = "stream" ->
charguer's avatar
charguer committed
162
      Coq_app (Coq_var "list", aux t)
163
   | Btyp_constr (id,[t]) when Path.name id = "Stream.stream_cell" || Path.name id = "stream_cell" ->
charguer's avatar
charguer committed
164 165 166 167 168
      Coq_app (Coq_var "list", aux t)
*)
(* REMARK: les Lazy provenant des patterns ne sont pas identique Predef.path_lazy_t *)


charguer's avatar
charguer committed
169 170
(** Translates a Caml type into a Coq type *)

charguer's avatar
charguer committed
171
let lift_typ_exp loc ty =
172
  lift_btyp loc (btyp_of_typ_exp ty)
charguer's avatar
charguer committed
173 174 175

(** Translates a Caml type scheme into a Coq type *)

charguer's avatar
charguer committed
176
let lift_typ_sch loc ty =
charguer's avatar
charguer committed
177 178
   let t = btyp_of_typ_sch_simple ty in
   let fv = fv_btyp ~through_arrow:false t in
charguer's avatar
charguer committed
179
   fv, lift_btyp loc t
charguer's avatar
charguer committed
180

charguer's avatar
charguer committed
181 182 183 184
let lift_typ_sch_as_forall loc ty =
   let fv, typ = lift_typ_sch loc ty in
   coq_forall_types fv typ

charguer's avatar
charguer committed
185 186
(** Translates the type of a Caml expression into a Coq type *)

charguer's avatar
charguer committed
187 188
let coq_typ loc e =
   lift_typ_exp loc (e.exp_type)
charguer's avatar
charguer committed
189 190 191

(** Translates the type of a Caml pattern into a Coq type *)

charguer's avatar
charguer committed
192 193
let coq_typ_pat loc p =
   lift_typ_exp loc (p.pat_type)
charguer's avatar
charguer committed
194 195 196 197 198

(** Decompose "A.B.s" as ("A.B","s") *)

let rec path_decompose = function
    Pident id -> ("", Ident.name id)
199
  | Pdot(p, s, pos) ->
charguer's avatar
charguer committed
200 201
      let (f,r) = path_decompose p in
      (f ^ r ^ ".", s)
charguer's avatar
charguer committed
202
  | Papply(p1, p2) -> unsupported_noloc "application in paths"
charguer's avatar
charguer committed
203 204 205 206


(** Extracts a record path_name / path from a type *)

207 208 209
let get_record_decomposed_name_for_exp e =
   let b = btyp_of_typ_exp (e.exp_type) in
   match b with
charguer's avatar
charguer committed
210 211 212 213 214 215 216 217 218 219 220 221
   | Btyp_constr (p,_) -> path_decompose (lift_path p)
   | _ -> failwith "illegal argument for get_record_decomposed_name_for_exp"



(*#########################################################################*)
(* ** Type arity functions *)

(** Get the number of type arguments of a (polymorphic) free variable *)

let typ_arity_var env x =
   match x with
222
   | Path.Pident id ->
charguer's avatar
charguer committed
223 224 225 226 227 228 229 230 231 232 233 234 235
      begin try Ident.find_same id env
      with Not_found -> 0 end
   | _ -> 0

(** Get the number of type arguments of a (polymorphic) data constructor *)

let typ_arity_constr c =
   match (c.cstr_res).desc with
   | Tconstr (_,ts,_) -> List.length ts
   | _ -> failwith "typ_arity_constr: result type of constructor is not a type constructor"

(** Translate a Caml data constructor into a Coq expression *)

charguer's avatar
charguer committed
236
(* DEPRECATED: attempt to type the constructor is problematic,
237
   because the type [ty] might not have a type constructor
charguer's avatar
charguer committed
238 239
   that is the one from the definition of the constructor. E.g.
     type 'a t = A of 'a
240
     type 'a mylist = 'a t list
charguer's avatar
charguer committed
241 242 243
     let empty : 'a mylist = []  ---> this is not 'a list.

  let coq_of_constructor_DEPRECATED loc p c ty =
244 245
     let typs =
        match btyp_of_typ_exp ty with
charguer's avatar
charguer committed
246 247 248 249 250 251 252 253 254 255
        | Btyp_constr (id,ts) -> List.map (lift_btyp loc) ts
        | _ -> failwith "coq_of_constructor: constructor has a type that is not a type constructor"
        in
     let x = string_of_path p in
     (* TODO: fixme, this can be hacked by rebinding None, Some, or :: ..*)
     let coq_name, arity =
        match find_builtin_constructor x with
        | None -> lift_path_name p, (typ_arity_constr c)
        | Some (coq_name,arity) -> coq_name, arity
        in
256
      if typs = []
charguer's avatar
charguer committed
257 258 259
        then coq_var coq_name
        else coq_apps (coq_var_at coq_name) typs
     (* DEPRECATED: coq_app_var_wilds coq_name arity *)
260 261

   | Tpat_construct (path, c, ps) ->
charguer's avatar
charguer committed
262 263 264 265 266 267 268
      coq_apps (coq_of_constructor loc path c p.pat_type) (List.map aux ps)
   | Texp_construct (p, c, es) ->
      coq_apps (coq_of_constructor loc p c e.exp_type) (List.map aux es)

*)

let coq_of_constructor loc p c args ty =
charguer's avatar
charguer committed
269
   let x = string_of_path p in
charguer's avatar
charguer committed
270
   let coq_name, _arity =
charguer's avatar
charguer committed
271
      match find_builtin_constructor x with
charguer's avatar
charguer committed
272
      | None -> lift_path_name p, (typ_arity_constr c)
charguer's avatar
charguer committed
273 274
      | Some (coq_name,arity) -> coq_name, arity
      in
charguer's avatar
charguer committed
275 276 277 278
  let constr = coq_var coq_name in
  let typ = lift_typ_exp loc ty in
  coq_annot (coq_apps constr args) typ

charguer's avatar
charguer committed
279 280 281 282 283 284 285

(*#########################################################################*)
(* ** Lifting of patterns *)

(** Compute the free variables of a pattern *)

let rec pattern_variables p : typed_vars = (* ignores aliases *)
charguer's avatar
charguer committed
286
   let loc = p.pat_loc in
charguer's avatar
charguer committed
287 288
   let aux = pattern_variables in
   match p.pat_desc with
charguer's avatar
charguer committed
289
   | Tpat_any -> not_in_normal_form loc "wildcard patterns remain after normalization"
charguer's avatar
charguer committed
290
   | Tpat_var s -> [var_name (Ident.name s), coq_typ_pat loc p]
charguer's avatar
charguer committed
291 292 293 294 295
   | Tpat_alias (p, s) -> aux p
   | Tpat_constant c -> []
   | Tpat_tuple l -> list_concat_map aux l
   | Tpat_construct (p, c, ps) -> list_concat_map aux ps
   | Tpat_lazy p1 -> aux p1
charguer's avatar
charguer committed
296 297 298 299
   | Tpat_variant (_,_,_) -> unsupported loc "variant patterns"
   | Tpat_record _ -> unsupported loc "record patterns"
   | Tpat_array pats -> unsupported loc "array patterns"
   | Tpat_or (_,p1,p2) -> unsupported loc "or patterns"
charguer's avatar
charguer committed
300 301 302 303

(** Translate a Caml pattern into a Coq expression, and
    ignores the aliases found in the pattern *)

304
let rec lift_pat ?(through_aliases=true) p : coq =
charguer's avatar
charguer committed
305
   let loc = p.pat_loc in
charguer's avatar
charguer committed
306 307
   let aux = lift_pat ~through_aliases:through_aliases in
   match p.pat_desc with
308
   | Tpat_var s ->
charguer's avatar
charguer committed
309
      Coq_var (var_name (Ident.name s))
310
   | Tpat_constant (Const_int n) ->
charguer's avatar
charguer committed
311
      Coq_int n
312
   | Tpat_tuple l ->
charguer's avatar
charguer committed
313
      Coq_tuple (List.map aux l)
314
   | Tpat_construct (path, c, ps) ->
charguer's avatar
charguer committed
315
      coq_of_constructor loc path c (List.map aux ps) p.pat_type
316
   | Tpat_alias (p, ak) ->
charguer's avatar
charguer committed
317
      begin match ak with
318
      | TPat_alias id ->
charguer's avatar
charguer committed
319
          if through_aliases then aux p else Coq_var (var_name (Ident.name id))
320 321
      | TPat_constraint ty ->
          let typ = lift_typ_exp loc ty.ctyp_type in
charguer's avatar
charguer committed
322
          Coq_annot (aux p, typ)
323
      | TPat_type pp -> aux p
charguer's avatar
charguer committed
324 325 326
      end
   | Tpat_lazy p1 ->
      aux p1
charguer's avatar
charguer committed
327 328 329 330 331 332
   | Tpat_record _ -> unsupported loc "record patterns" (* todo! *)
   | Tpat_array pats -> unsupported loc "array patterns" (* todo! *)
   | Tpat_constant _ -> unsupported loc "only integer constant are supported"
   | Tpat_any -> not_in_normal_form loc "wildcard patterns remain after normalization"
   | Tpat_variant (_,_,_) -> unsupported loc "variant patterns"
   | Tpat_or (_,p1,p2) -> unsupported loc "or patterns in depth"
charguer's avatar
charguer committed
333 334 335 336

(** Extracts the aliases from a Caml pattern, in the form of an
    association list mapping variables to Coq expressions *)

337
let pattern_aliases p : (typed_var*coq) list =
charguer's avatar
charguer committed
338
   let loc = p.pat_loc in
charguer's avatar
charguer committed
339 340 341 342 343 344
   let rec aux p =
      match p.pat_desc with
      | Tpat_var s -> []
      | Tpat_constant (Const_int n) -> []
      | Tpat_tuple l -> list_concat_map aux l
      | Tpat_construct (p, c, ps) -> list_concat_map aux ps
345
      | Tpat_alias (p1, ak) ->
charguer's avatar
charguer committed
346 347
          begin match ak with
          | TPat_alias id ->
charguer's avatar
charguer committed
348
             ((Ident.name id, coq_typ_pat loc p), lift_pat ~through_aliases:false p1) :: (aux p1)
charguer's avatar
charguer committed
349 350 351 352
          | TPat_constraint _ -> aux p1
          | TPat_type pp -> aux p1
         end
      | Tpat_lazy p1 ->  aux p1
charguer's avatar
charguer committed
353 354 355 356 357
      | Tpat_record _ -> unsupported loc "record patterns" (* todo! *)
      | Tpat_array pats -> unsupported loc "array patterns" (* todo! *)
      | Tpat_constant _ -> unsupported loc "only integer constant are supported"
      | Tpat_any -> not_in_normal_form loc "wildcard patterns remain after normalization"
      | Tpat_variant (_,_,_) -> unsupported loc "variant patterns"
358
      | Tpat_or (_,p1,p2) -> unsupported loc "or patterns"
charguer's avatar
charguer committed
359 360 361 362 363
      in
   List.rev (aux p)


(*#########################################################################*)
charguer's avatar
charguer committed
364
(* ** Helper functions for various things *)
charguer's avatar
charguer committed
365 366

let register_cf x =
charguer's avatar
charguer committed
367
   Coqtop_custom (sprintf "Hint Extern 1 (RegisterCF %s) => CFHeader_Provide %s." x (cf_axiom_name x))
368
   (* DEPRECATED
charguer's avatar
charguer committed
369 370
      Coqtop_register ("CFML.CFPrint.database_cf", x, cf_axiom_name x)
    *)
charguer's avatar
charguer committed
371 372

let register_spec x v =
charguer's avatar
charguer committed
373
   Coqtop_register ("CFML.CFPrint.database_spec", x, v)
charguer's avatar
charguer committed
374

charguer's avatar
charguer committed
375

charguer's avatar
charguer committed
376
(* TODO: rewrite this function by using a normalization function that returns p *)
377 378 379
let rec prefix_for_label typ =
  match typ.desc with
  | Tconstr (p, _, _) -> lift_path_name p
charguer's avatar
charguer committed
380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395
  | Tlink t -> prefix_for_label t
  | _ -> failwith "string_of_label: type of a record should be a Tconstr or Tlink"
  (*
  | Tvar -> failwith "x1"
  | Tarrow _ -> failwith "x2"
  | Ttuple  _ -> failwith "x3"
  | Tconstr _ -> failwith "x4"
  | Tobject  _ -> failwith "x5"
  | Tfield _ -> failwith "x6"
  | Tnil _ -> failwith "x7"
  | Tsubst  _ -> failwith "x9"
  | Tvariant  _ -> failwith "x10"
  | Tunivar -> failwith "x11"
  | Tpoly  _ -> failwith "x12"
  *)

396
(* DEPRECATED
charguer's avatar
charguer committed
397 398 399 400 401
let string_of_label_with prefix lbl =
  prefix ^ "_" ^ lbl.lbl_name

let string_of_label typ lbl =
  string_of_label_with (prefix_for_label typ) lbl
charguer's avatar
charguer committed
402
*)
charguer's avatar
charguer committed
403

charguer's avatar
charguer committed
404 405 406 407 408

(*#########################################################################*)
(* ** Helper functions for primitive functions *)

let simplify_apply_args loc oargs =
409
  List.map (function (lab, Some e, Required) -> e | _ -> unsupported loc "optional arguments") oargs
charguer's avatar
charguer committed
410

411
let get_qualified_pervasives_name f =
charguer's avatar
charguer committed
412
   let name = Path.name f in
413
   if !Clflags.nopervasives
charguer's avatar
charguer committed
414 415
      then "Pervasives." ^ name  (* unqualified name when from inside Pervasives *)
      else name  (* qualified name otherwise *)
charguer's avatar
charguer committed
416 417

let exp_find_inlined_primitive e oargs =
charguer's avatar
charguer committed
418 419 420 421 422
   let loc = e.exp_loc in
   let args = simplify_apply_args loc oargs in
   match e.exp_desc with
   | Texp_ident (f,d) ->
      let name = get_qualified_pervasives_name f in
charguer's avatar
charguer committed
423

charguer's avatar
charguer committed
424
      let _debug() =
charguer's avatar
charguer committed
425 426
         Printf.printf "exp_find_inlined_primitive: %s\n arity: %d\n name: %s\n" (Path.name f) (List.length args) name
         in
charguer's avatar
charguer committed
427
      (* _debug(); *)
charguer's avatar
charguer committed
428

429
      begin match args with
430

431 432 433
      | [n; {exp_desc = Texp_constant (Const_int m)}]
           when m <> 0
             && List.mem name ["Pervasives.mod"; "Pervasives./"] ->
charguer's avatar
charguer committed
434 435 436 437
           begin match find_inlined_primitive name with
           | Some (Primitive_binary_div_or_mod, coq_name) -> Some coq_name
           | _ -> None
           end
charguer's avatar
charguer committed
438

439 440
       | [e1; e2]
           when List.mem name ["Pervasives.&&"; "Pervasives.||"] ->
charguer's avatar
charguer committed
441 442 443 444
           begin match find_inlined_primitive (Path.name f) with
           | Some (Primitive_binary_lazy, coq_name) -> Some coq_name
           | _ -> None
           end
charguer's avatar
charguer committed
445

446 447
       | [e1; e2]
           when List.mem name ["Pervasives.="; "Pervasives.<>"; "Pervasives.<=";
charguer's avatar
charguer committed
448
                               "Pervasives.>="; "Pervasives.<"; "Pervasives.>";
449 450
                               "Pervasives.min"; "Pervasives.max"; ] ->
           let is_number =
charguer's avatar
charguer committed
451 452 453
              try Ctype.unify e1.exp_env e1.exp_type ((*instance*) Predef.type_int); true
              with _ -> false
              (*begin match btyp_of_typ_exp e1.exp_type with
charguer's avatar
charguer committed
454
              | Btyp_constr (id,[]) when Path.name id = "int" -> true
charguer's avatar
charguer committed
455
              | _ -> false
charguer's avatar
charguer committed
456 457
              end *)
              in
charguer's avatar
charguer committed
458
             (* Remark: by typing, [e2] has the same type as [e1] *)
charguer's avatar
charguer committed
459 460 461
           if not is_number then begin
             if List.mem name [ "Pervasives.="; "Pervasives.<>"; ]
               then None
charguer's avatar
charguer committed
462 463 464
               (* TODO: improve using type unification *)
               else (* warning loc *)
               unsupported loc (Printf.sprintf "comparison operators on non integer arguments (here, %s)" (string_of_type_exp e1.exp_type));
charguer's avatar
charguer committed
465 466 467
           end else begin match find_inlined_primitive name with
              | Some (Primitive_binary_only_numbers, coq_name) -> Some coq_name
              | _ -> failwith ("in exp_find_inlined_primitive, could not find the coq translation of the function: " ^ name)
charguer's avatar
charguer committed
468 469
           end

470
       | _ ->
charguer's avatar
charguer committed
471 472 473 474 475 476 477 478 479 480 481 482 483 484
           let arity = List.length args in
           begin match find_inlined_primitive name with
           | Some (Primitive_unary, coq_name) when arity = 1 -> Some coq_name
           | Some (Primitive_binary, coq_name) when arity = 2 -> Some coq_name
           | _ -> None
           end
           (* debug: Printf.printf "exp_find_inlined_primitive: %s %d\n"  (Path.name f)  (List.length args);
           if r = None then Printf.printf "failed\n"; *)

       end

    | _ -> None


charguer's avatar
charguer committed
485

charguer's avatar
charguer committed
486 487 488
(*#########################################################################*)
(* ** Lifting of values *)

489
(** Translate a Caml identifier into a Coq identifier, possibly
charguer's avatar
charguer committed
490 491 492 493
    applied to wildcards for taking type applications into account *)

let lift_exp_path env p =
   match find_primitive (Path.name p) with
494
   | None ->
charguer's avatar
charguer committed
495
      let x = lift_path_name (var_path p) in
charguer's avatar
charguer committed
496
      coq_app_var_wilds x (typ_arity_var env p)
497 498
   | Some y ->
      Coq_var y
charguer's avatar
charguer committed
499

500
(** Translate a Caml value into a Coq value. Fails if the Coq
charguer's avatar
charguer committed
501 502
    expression provided is not a value. *)

503
let rec lift_val env e =
charguer's avatar
charguer committed
504
   let loc = e.exp_loc in
charguer's avatar
charguer committed
505
   let aux = lift_val env in
charguer's avatar
charguer committed
506 507
   let fail () =
     not_in_normal_form loc ("in liftval: " ^ Print_tast.string_of_expression false e) in
charguer's avatar
charguer committed
508
   match e.exp_desc with
509 510 511
   | Texp_ident (p,d) ->
     lift_exp_path env p
   | Texp_open (p, _) ->
charguer's avatar
charguer committed
512 513 514
     assert false
   | Texp_constant (Const_int n) ->
      Coq_int n
515
   | Texp_constant _ ->
charguer's avatar
charguer committed
516
      unsupported loc "only integer constant are supported"
517
   | Texp_tuple el ->
charguer's avatar
charguer committed
518 519
      Coq_tuple (List.map aux el)
   | Texp_construct (p, c, es) ->
charguer's avatar
charguer committed
520
      coq_of_constructor loc p c (List.map aux es) e.exp_type
521
   | Texp_record (l, opt_init_expr) ->
charguer's avatar
charguer committed
522
       if opt_init_expr <> None then unsupported loc "record-with expression"; (* todo *)
charguer's avatar
charguer committed
523 524 525 526 527 528
       if List.length l < 1 then failwith "record should have at least one field";
       let labels = ((fun (p,li,ei) -> li) (List.hd l)).lbl_all in
       let args = Array.make (Array.length labels) (Coq_var "dummy") in
       let register_arg lbl v =
          Array.iteri (fun i lbli -> if lbl.lbl_name = lbli.lbl_name then args.(i) <- v) labels in
       List.iter (fun (p,lbl,v) -> register_arg lbl (aux v)) l;
charguer's avatar
charguer committed
529
       let constr = record_constructor_name_from_type (prefix_for_label (e.exp_type)) in
530
       let typ_args =
charguer's avatar
charguer committed
531
          match btyp_of_typ_exp e.exp_type with
charguer's avatar
charguer committed
532
          | Btyp_constr (id,ts) -> List.map (lift_btyp loc) ts
charguer's avatar
charguer committed
533 534 535
          | _ -> failwith "record should have a type-constructor as type"
          in
       coq_apps (coq_var_at constr) (typ_args @ Array.to_list args)
charguer's avatar
charguer committed
536 537 538 539 540 541 542
   | Texp_apply (funct, oargs) ->
      let fo = exp_find_inlined_primitive funct oargs in
      let f = match fo with
         | Some f -> f
         | _ -> fail()
         in
      let args = simplify_apply_args loc oargs in
charguer's avatar
charguer committed
543
      coq_apps (Coq_var f) (List.map aux args)
544
   | Texp_lazy e ->
charguer's avatar
charguer committed
545
      aux e
546
   | Texp_constraint (e, Some ty, None) ->
charguer's avatar
charguer committed
547
      let typ = lift_typ_exp loc ty.ctyp_type in
charguer's avatar
charguer committed
548
      Coq_annot (aux e, typ)
charguer's avatar
charguer committed
549
   | _ -> fail()
charguer's avatar
charguer committed
550

551
   (* --uncomment for debugging
charguer's avatar
charguer committed
552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577
   | Texp_function _ -> not_in_normal_form loc "function"
   | Texp_apply _ -> not_in_normal_form loc "apply"
   | Texp_assertfalse -> not_in_normal_form loc "assert false"
   | Texp_try(body, pat_expr_list) -> not_in_normal_form loc "try expression"
   | Texp_variant(l, arg) ->  not_in_normal_form loc "variant expression"
   | Texp_setfield(arg, p, lbl, newval) -> not_in_normal_form loc "set-field expression"
   | Texp_array expr_list -> not_in_normal_form loc "array expressions"
   | Texp_ifthenelse(cond, ifso, None) -> not_in_normal_form loc "if-then-without-else expressions"
   | Texp_sequence(expr1, expr2) -> not_in_normal_form loc "sequence expressions"
   | Texp_while(cond, body) -> not_in_normal_form loc "while expressions"
   | Texp_for(param, low, high, dir, body) -> not_in_normal_form loc "for expressions"
   | Texp_when(cond, body) -> not_in_normal_form loc "when expressions"
   | Texp_send(_ , _, _) -> not_in_normal_form loc "send expressions"
   | Texp_new (cl, _) -> not_in_normal_form loc "new expressions"
   | Texp_instvar(path_self, path) -> not_in_normal_form loc "inst-var expressions"
   | Texp_setinstvar(path_self, path, expr) -> not_in_normal_form loc "set-inst-var expressions"
   | Texp_override(path_self, modifs) -> not_in_normal_form loc "override expressions"
   | Texp_letmodule(id, modl, body) -> not_in_normal_form loc "let-module expressions"
   | Texp_assert (cond) -> not_in_normal_form loc "assert expressions"
   | Texp_object (_, _) -> not_in_normal_form loc "object expressions"
   | Texp_poly _  -> not_in_normal_form loc "object expressions"
   | Texp_newtype _  -> not_in_normal_form loc "object expressions"
   | Texp_pack _  -> not_in_normal_form loc "object expressions"
   | Texp_let _ -> not_in_normal_form loc "let"
   | Texp_match _ -> not_in_normal_form loc "match"
   | Texp_field _ -> not_in_normal_form loc "field"
charguer's avatar
charguer committed
578 579 580 581 582 583 584 585 586 587 588
   *)

   (* --todo: could be a value in a purely-functional setting
   | Texp_field (e, lbl) ->
       let typ = e.exp_type in
       Coq_app (Coq_var (string_of_label typ lbl), aux e) *)


(*#########################################################################*)
(* ** Helper functions for producing label names *)

charguer's avatar
charguer committed
589 590
(* FOR FUTURE USE *)

591
let counter_local_label =
charguer's avatar
charguer committed
592
   ref 0
593
let get_next_local_label () =
charguer's avatar
charguer committed
594 595
   incr counter_local_label;
   "_m" ^ (string_of_int !counter_local_label)
596
let reset_local_labels() =
charguer's avatar
charguer committed
597 598
   counter_local_label := 0

599
let used_labels : (var list) ref =
charguer's avatar
charguer committed
600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616
   ref []
let reset_used_labels () =
   used_labels := []
let add_used_label x =
   if not (List.mem x !used_labels)
      then used_labels := x :: !used_labels

let cfg_extract_labels () =
   let labs = List.rev !used_labels in
   let cft = [ Cftop_coqs (list_mapi (fun i x -> Coqtop_label (x,i+1)) labs) ] in
   reset_used_labels();
   cft


(*#########################################################################*)
(* ** Helper functions for names *)

617
(** Takes a pattern that is expected to be reduced simply to an identifier,
charguer's avatar
charguer committed
618 619 620 621 622 623 624 625
    and returns this identifier *)

let rec pattern_ident p =
   match p.pat_desc with
   | Tpat_var s -> s
   | Tpat_alias (p1,_) -> pattern_ident p1
   | _ -> failwith ("pattern_ident: the pattern is not a name: " ^ (Print_tast.string_of_pattern false p))

626
(** Takes a pattern that is expected to be reduced simply to an identifier,
charguer's avatar
charguer committed
627 628 629 630 631
    and returns the name of this identifier *)

let pattern_name p =
   Ident.name (pattern_ident p)

charguer's avatar
charguer committed
632 633 634
(** Takes a function name and encodes its name in case of an infix operator *)

let pattern_name_protect_infix p =
charguer's avatar
charguer committed
635
   var_name (pattern_name p)
charguer's avatar
charguer committed
636

charguer's avatar
charguer committed
637 638 639 640 641 642 643 644 645 646 647
(** An alternative version of function extract_label_names, for obtaining record labels *)

let rec extract_label_names_simple env ty =
  let ty = Ctype.repr ty in
  match ty.desc with
  | Tconstr (path, _, _) ->
      let td = Env.find_type path env in
      begin match td.type_kind with
      | Type_record (fields, _) ->
          List.map (fun (name, _, _) -> name) fields
      | Type_abstract when td.type_manifest <> None ->
charguer's avatar
charguer committed
648
          unsupported_noloc "building of a record with abstract type"
charguer's avatar
charguer committed
649 650 651 652 653
      | _ -> assert false
      end
  | _ -> assert false


charguer's avatar
charguer committed
654 655 656 657 658 659 660 661 662 663
(*#########################################################################*)
(* ** Helper functions for fvs (type variables) *)


let show_fvs title fvs =
   Format.fprintf Format.err_formatter "%s = %s\n" title (show_list show_str " , " fvs)

(* needs to be called only after typing the body of the definition
   associated with the pattern, so as to know which names are actually used. *)

664
let get_fvs_typ loc fvs typ =
charguer's avatar
charguer committed
665
  let typ = lift_typ_exp loc typ in
charguer's avatar
charguer committed
666
  let fvs = List.map name_of_type_var (List.filter typvar_is_used fvs) in
charguer's avatar
charguer committed
667 668 669 670
  (fvs, [], typ)

  (* DEPRECATED
  let fvs_typ, typ = lift_typ_sch loc typ in
charguer's avatar
charguer committed
671
  let fvs = List.map name_of_type_var (List.filter typvar_is_used fvs) in
charguer's avatar
charguer committed
672 673 674 675
  if Settings.debug_generic then begin
     show_fvs "fvs_typ" fvs_typ;
     show_fvs "fvs" fvs;
  end;
676
  if not (list_is_included fvs_typ fvs)
charguer's avatar
charguer committed
677
    then failwith "fvs_typ not included in fvs for let binding";
678
  let fvs_strict = fvs_typ in
charguer's avatar
charguer committed
679 680 681 682 683
  let fvs_others = list_minus fvs fvs_strict in
  (fvs_strict, fvs_others, typ)
  *)


charguer's avatar
charguer committed
684 685 686 687 688
(*#########################################################################*)
(* ** Characteristic formulae for expressions *)

(** Translate a Caml expression into its Coq characteristic formula *)

689
let rec cfg_exp env e =
charguer's avatar
charguer committed
690
   let loc = e.exp_loc in
charguer's avatar
charguer committed
691 692 693
   let aux = cfg_exp env in
   let lift e = lift_val env e in
   let ret e = Cf_ret (lift e) in
charguer's avatar
charguer committed
694 695
   let not_normal ?s:(s="") () =
      not_in_normal_form loc (s ^ Print_tast.string_of_expression false e) in
charguer's avatar
charguer committed
696 697 698 699 700 701 702 703
   match e.exp_desc with
   | Texp_ident (x,d) -> ret e
   | Texp_open (p, {exp_desc = Texp_ident _}) -> assert false
   | Texp_constant cst -> ret e
   | Texp_tuple el -> ret e
   | Texp_construct(p, cstr, args) -> ret e
   (* TODO: only in purely function setting:   | Texp_record (lbl_expr_list, opt_init_expr) -> ret e*)

704 705
   | Texp_record (_, _) ->
     cfg_record env e
charguer's avatar
charguer committed
706

charguer's avatar
charguer committed
707
   | Texp_apply (funct, oargs) when (exp_find_inlined_primitive funct oargs <> None) -> ret e
charguer's avatar
charguer committed
708

charguer's avatar
charguer committed
709
   | Texp_function (_, pat_expr_list, partial) -> not_normal ~s:"The function involved has not been lifted properly during normalization;\n check the normalized file in _output folder.\n" ()
charguer's avatar
charguer committed
710 711

   | Texp_let(rf, fvs, pat_expr_list, body) ->
712 713

      let is_let_fun =
charguer's avatar
charguer committed
714 715 716 717 718
         match (snd (List.hd pat_expr_list)).exp_desc with
         | Texp_function (_,_,_) -> true
         | Texp_constraint ({exp_desc = Texp_function (_,_,_)},_,_) -> true (* todo: generalize *)
         | _ -> false in

719 720 721 722 723 724
      let is_let_record_new =
         match (snd (List.hd pat_expr_list)).exp_desc with
         | Texp_record (_,_) -> true
         | Texp_constraint ({exp_desc = Texp_record (_,_)},_,_) -> true (* todo: generalize *)
         | _ -> false in

charguer's avatar
charguer committed
725 726
      (* binding of functions, possibly mutually-recursive *)
      if is_let_fun then begin
727
        let env' = match rf with
charguer's avatar
charguer committed
728 729 730 731
           | Nonrecursive -> env
           | Recursive -> env
              (* --todo: add better support for local polymorphic recursion
              List.fold_left (fun (pat,bod) acc -> Ident.add (pattern_ident pat) 0 acc) env pat_expr_list *)
charguer's avatar
charguer committed
732
           | Default -> unsupported loc "Default recursion mode"
charguer's avatar
charguer committed
733
           in
charguer's avatar
charguer committed
734
        let ncs = List.map (fun (pat,bod) -> (pattern_name_protect_infix pat, cfg_func env' fvs pat bod)) pat_expr_list in
735
        let cf_body = cfg_exp env' body in
charguer's avatar
charguer committed
736
        add_used_label (fst (List.hd ncs));
charguer's avatar
charguer committed
737
        Cf_fun (ncs, cf_body)
charguer's avatar
charguer committed
738 739 740
        (* --todo: check what happens with recursive types *)

      (* let-binding of a single value *)
741
      end else begin
charguer's avatar
charguer committed
742 743
        if (List.length pat_expr_list <> 1) then not_normal();
        let (pat,bod) = List.hd pat_expr_list in
charguer's avatar
charguer committed
744
        let x = pattern_name_protect_infix pat in
745

charguer's avatar
charguer committed
746
        (* value let-binding *)
747
        if Typecore.is_nonexpansive bod then begin
charguer's avatar
charguer committed
748

749 750 751
           let v =
             try lift_val env bod
             with Not_in_normal_form (loc2, s) ->
charguer's avatar
charguer committed
752
                raise (Not_in_normal_form (loc2, s ^ " (only value can satisfy the value restriction)"))
charguer's avatar
charguer committed
753
             in
charguer's avatar
charguer committed
754
           let (fvs_strict, fvs_others, typ) = get_fvs_typ loc fvs pat.pat_type in
755
           if fvs_others != []
charguer's avatar
charguer committed
756
              then unsupported loc "polymorphic let-value binding whose type-checking involves type variables that are not contained in the result type.";
charguer's avatar
charguer committed
757 758 759
           let env' = Ident.add (pattern_ident pat) (List.length fvs_strict) env in
           let cf = cfg_exp env' body in
           add_used_label x;
charguer's avatar
charguer committed
760
           Cf_val (x, fvs_strict, typ, v, cf)
charguer's avatar
charguer committed
761 762 763

        (* term let-binding *)
        end else begin
764

charguer's avatar
charguer committed
765 766 767 768 769 770 771 772 773
           (* DEPRECATED
              if fvs = [] then begin
                 (* Simple form without polymorphism *)
                 let cf1 = cfg_exp env bod in
                 let typ = lift_typ_exp loc pat.pat_type in
                 let env' = Ident.add (pattern_ident pat) 0 env in
                 let cf2 = cfg_exp env' body in
                 add_used_label x;
                 Cf_let ((x,typ), cf1, cf2)
774 775
              end else
              (* General form with polymorphism *)
charguer's avatar
charguer committed
776 777 778 779
           *)

            begin

780 781 782 783 784 785 786
              let cf1 =
                (* Recursive record term let-binding *)
                if is_let_record_new && rf = Recursive then
                  cfg_record ~record_name:x env bod
                else
                  cfg_exp env bod
              in
charguer's avatar
charguer committed
787 788 789 790
              let fvs_typ, typ = lift_typ_sch loc pat.pat_type in
              (* fvs_typ contains all free type variables in the type;
                 and thus too many w.r.t. to the ones of interest here *)
              let fvs = List.map name_of_type_var (List.filter typvar_is_used fvs) in
791
              let fvs_strict = list_intersect fvs fvs_typ in
charguer's avatar
charguer committed
792 793 794 795
              let fvs_others = list_minus fvs fvs_strict in
              let env' = Ident.add (pattern_ident pat) (List.length fvs_strict) env in
              let cf2 = cfg_exp env' body in
              add_used_label x;
796
              if fvs_strict = [] && fvs_others = []
charguer's avatar
charguer committed
797 798 799 800 801 802 803 804 805
                then Cf_let ((x,typ), cf1, cf2)
                else Cf_let_poly (x, fvs_strict, fvs_others, typ, cf1, cf2)

                  (* DEPRECATED
                     Printf.printf "fvs_strict = %s\n" (show_list show_str " , " fvs_strict);
                     Printf.printf "fvs_others = %s\n" (show_list show_str " , " fvs_others);
                     unsupported loc "relaxed value restriction";
                     not_in_normal_form loc ("(un value restriction) "
                        ^ (Print_tast.string_of_expression false e));*)
charguer's avatar
charguer committed
806
           end;
807

charguer's avatar
charguer committed
808 809 810 811 812 813

        end
      end

   | Texp_ifthenelse (cond, ifso, Some ifnot) ->
      (* old: Cf_caseif (aux cond, aux ifso, aux ifnot) *)
814
      Cf_caseif (lift cond, aux ifso, aux ifnot)
charguer's avatar
charguer committed
815 816

   | Texp_apply (funct, oargs) ->
charguer's avatar
charguer committed
817
      let args = simplify_apply_args loc oargs in
charguer's avatar
charguer committed
818 819
      let tr = coq_typ loc e in
      let ts = List.map (coq_typ loc) args in
820
      Cf_app (ts, tr, lift funct, List.map lift args)
charguer's avatar
charguer committed
821 822 823 824 825

   | Texp_match (arg, pat_expr_list, partial) ->
      let tested = lift arg in
      let conclu = match partial with Partial -> Cf_fail | Total -> Cf_done in
      let cfg_case (pat,body) acc =
826 827
         let whenopt, cfbody =
            match body.exp_desc with
charguer's avatar
charguer committed
828
            | Texp_when (econd, ebody) ->
829 830 831
                let w =
                   try lift_val env econd
                   with Not_in_normal_form (loc2, s) ->
charguer's avatar
charguer committed
832
                      raise (Not_in_normal_form (loc2, s ^ " (Only total expressions are allowed in when clauses)"))
charguer's avatar
charguer committed
833 834 835 836 837 838 839 840 841
                   in
                Some w, aux ebody
            | _ -> None, aux body
            in
         Cf_case (tested, pattern_variables pat, lift_pat pat, whenopt, pattern_aliases pat, cfbody, acc) in
      let label = get_next_local_label() in
      add_used_label label;
      Cf_match (label, List.length pat_expr_list, List.fold_right cfg_case pat_expr_list conclu)

842
   | Texp_assert e ->
charguer's avatar
charguer committed
843 844
      Cf_assert (aux e)

845
   | Texp_assertfalse ->
charguer's avatar
charguer committed
846 847
      Cf_fail

848
   | Texp_lazy e ->
charguer's avatar
charguer committed
849 850
      aux e

851
   | Texp_sequence(expr1, expr2) ->
charguer's avatar
charguer committed
852 853
      Cf_seq (aux expr1, aux expr2)

854
   | Texp_while(cond, body) ->
charguer's avatar
charguer committed
855 856
      Cf_while (aux cond, aux body)

857 858
   | Texp_for(param, low, high, caml_dir, body) ->
      let dir =
charguer's avatar
charguer committed
859 860 861
        match caml_dir with
        | Upto -> For_loop_up
        | Downto -> For_loop_down
862 863 864 865
      in
      let cf_body = aux body in
      let cf_body = if !Mytools.use_credits then Cf_pay cf_body else cf_body in
      Cf_for (dir, Ident.name param, lift low, lift high, cf_body)
charguer's avatar
charguer committed
866

867
   | Texp_array args ->
charguer's avatar
charguer committed
868
      let arg = coq_list (List.map lift args) in
869
      let targ = (* ['a], obtained by extraction from ['a array]. *)
charguer's avatar
charguer committed
870
         match btyp_of_typ_exp e.exp_type with
charguer's avatar
charguer committed
871
         | Btyp_constr (id,[t]) when Path.name id = "array" -> lift_btyp loc t
charguer's avatar
charguer committed
872 873 874
         | _ -> failwith "Texp_array should always have type ['a array]"
         in
      let ts = coq_apps (Coq_var "Coq.Init.Datatypes.list") [targ] in
charguer's avatar
charguer committed
875
      let tr = coq_typ loc e in (* 'a array *)
876
      let func = Coq_var "Array_ml.of_list" in
charguer's avatar
charguer committed
877
      Cf_app ([ts], tr, func, [arg])
charguer's avatar
charguer committed
878

879 880
   | Texp_field (arg, p, lbl) ->
      let tr = coq_typ loc e in
charguer's avatar
charguer committed
881
      let ts = coq_typ loc arg in (* todo: check it is always 'loc' *)
charguer's avatar
charguer committed
882 883
      let func = Coq_var "CFML.CFApp.record_get" in
      let field = Coq_var (record_field_name lbl.lbl_name) in
884
      Cf_app ([ts; coq_nat], tr, func, [lift arg; field])
charguer's avatar
charguer committed
885
      (* DEPRECATED
charguer's avatar
charguer committed
886
      let func = Coq_var (record_field_get_name lbl.lbl_name) in
887
      Cf_app ([ts], tr, func, [lift arg])
charguer's avatar
charguer committed
888
      *)
charguer's avatar
charguer committed
889

890
   | Texp_setfield(arg, p, lbl, newval) ->
charguer's avatar
charguer committed
891
      let ts1 = coq_typ loc arg in (* todo: check it is always 'loc' *)
892
      let ts2 = coq_typ loc newval in
charguer's avatar
charguer committed
893
      let func = Coq_var "CFML.CFApp.record_set" in
charguer's avatar
charguer committed
894
      let field = Coq_var (record_field_name lbl.lbl_name) in
895
      Cf_app ([ts1; coq_nat; ts2], coq_unit, func, [lift arg; field; lift newval])
charguer's avatar
charguer committed
896
      (* DEPRECATED
charguer's avatar
charguer committed
897
      let func = Coq_var (record_field_set_name lbl.lbl_name) in
charguer's avatar
charguer committed
898 899
      Cf_app ([ts1;ts2], coq_unit, func, [lift arg; lift newval])
      *)
charguer's avatar
charguer committed
900

charguer's avatar
charguer committed
901 902 903 904 905 906 907 908 909 910 911 912 913 914 915
   | Texp_try(body, pat_expr_list) -> unsupported loc "try expression"
   | Texp_variant(l, arg) ->  unsupported loc "variant expression"
   | Texp_ifthenelse(cond, ifso, None) -> unsupported loc "if-then-without-else expressions should have been normalized"
   | Texp_when(cond, body) -> unsupported loc "when expressions outside of pattern matching"
   | Texp_send(_, _, _) -> unsupported loc "send expressions"
   | Texp_new (cl, _) -> unsupported loc "new expressions"
   | Texp_instvar(path_self, path) -> unsupported loc "inst-var expressions"
   | Texp_setinstvar(path_self, path, expr) -> unsupported loc "set-inst-var expressions"
   | Texp_override(path_self, modifs) -> unsupported loc "override expressions"
   | Texp_letmodule(id, modl, body) -> unsupported loc "let-module expressions"
   | Texp_object _ -> unsupported loc "object expressions"
   | Texp_poly (_,_) -> unsupported loc "poly"
   | Texp_newtype (_,_) -> unsupported loc "newtype"
   | Texp_pack _ -> unsupported loc "pack"
   | Texp_open (_,_) -> unsupported loc "open in term"
charguer's avatar
charguer committed
916 917
   | Texp_constraint (e, Some ty, None) -> aux e
      (* LATER: see if it is needed
charguer's avatar
charguer committed
918
      let typ = lift_typ_exp loc ty.ctyp_type in
charguer's avatar
charguer committed
919 920 921 922
      CF_annot (aux e, typ)
      *)
   | Texp_constraint (e, _, _) -> unsupported loc "advanced type constraint"

charguer's avatar
charguer committed
923 924 925

and cfg_func env fvs pat bod =
   let rec get_typed_args acc e =
charguer's avatar
charguer committed
926
      let loc = e.exp_loc in
charguer's avatar
charguer committed
927
      match e.exp_desc with
928
      | Texp_function (_,[p1,e1],partial)
charguer's avatar
charguer committed
929
      | Texp_constraint ({exp_desc = Texp_function (_,[p1,e1],partial)},_,_) ->
930
         if partial <> Total
charguer's avatar
charguer committed
931
            then not_in_normal_form loc (Print_tast.string_of_expression false e);
charguer's avatar
charguer committed
932
         get_typed_args ((pattern_name p1, coq_typ_pat loc p1)::acc) e1
charguer's avatar
charguer committed
933
      | _ -> List.rev acc, e
934
      in
charguer's avatar
charguer committed
935
   let loc = pat.pat_loc in
charguer's avatar
charguer committed
936
   let f = pattern_name_protect_infix pat in
charguer's avatar
charguer committed
937
   let targs, body = get_typed_args [] bod in
charguer's avatar
charguer committed
938
   let typ = lift_typ_exp loc body.exp_type in
charguer's avatar
charguer committed
939
   let cf_body = cfg_exp env body in
charguer's avatar
charguer committed
940
   let cf_body = if !Mytools.use_credits then Cf_pay cf_body else cf_body in
charguer's avatar
charguer committed
941
   (* fvs computation must come after cf_body *)
charguer's avatar
charguer committed
942
   let fvs = List.map name_of_type_var (List.filter typvar_is_used fvs) in
943
   Cf_body (f, fvs, targs, typ, cf_body)
charguer's avatar
charguer committed
944 945 946
   (* --todo: check if the set of type variables quantified is not too
      conservative. Indeed, some type variables may no longer occur. *)

947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973
and cfg_record ?(record_name = "_") env e =
  let loc = e.exp_loc in
  match e.exp_desc with
  | Texp_record (lbl_expr_list, opt_init_expr) ->
    if opt_init_expr <> None then unsupported loc "record-with";
    let named_args = List.map (fun (p,li,ei) -> (li.lbl_name,ei)) lbl_expr_list in
    let build_arg (name, arg) =
      let value = coq_apps coq_dyn_at [coq_typ loc arg; lift_val env arg] in
      Coq_tuple [Coq_var (record_field_name name); value]
      in
    let arg =
      Coq_fun ((record_name, coq_var "CFHeaps.loc"),
               coq_list (List.map build_arg named_args)) in
    Cf_record_new (arg)

  (* DEPRECATED
  let (pathfront,pathend) = get_record_decomposed_name_for_exp e in
  let func = Coq_var (pathfront ^ (record_make_name pathend)) in
  let fields_names = extract_label_names_scimple e.exp_env e.exp_type in
  let args =
     try List.map (fun name -> List.assoc name named_args) fields_names
     with Not_found -> failwith "some fields are missing in a record construction"
     in
  let tprod = coq_prod (List.map coq_typ args) in
  Cf_app ([tprod], loc_type, func, [Coq_tuple (List.map lift args)])
  *)
  | _ -> assert false
charguer's avatar
charguer committed
974 975 976 977 978 979 980

(*#########################################################################*)
(* ** Characteristic formulae for modules *)

(** Helper functions to find out the kind of a type declaration *)

let is_algebraic (name,dec) =
981
   match dec.typ_type.type_kind with Type_variant _ -> true | _ -> false
charguer's avatar
charguer committed
982 983

let is_type_abbrev (name,dec) =
984
   match dec.typ_type.type_kind with Type_abstract -> true | _ -> false
charguer's avatar
charguer committed
985 986

let is_type_record (name,dec) =
987
   match dec.typ_type.type_kind with Type_record _ -> true | _ -> false
charguer's avatar
charguer committed
988

989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005
let rec is_ignored_str_value (pat,exp) =
  is_ignored_exp exp

and is_ignored_exp exp =
   match exp.exp_desc with
   | Texp_constraint (e, _, _) ->
      is_ignored_exp e
   | Texp_sequence(expr1, expr2) ->
      is_ignored_exp expr1
   | Texp_function (_, pat_expr_list, _) ->
      List.exists is_ignored_str_value pat_expr_list
   | Texp_apply ({exp_desc = Texp_ident (f,_d)},
                [_, Some {exp_desc = Texp_constant (Const_string "CFML")}, _])
      when get_qualified_pervasives_name f = "Pervasives.ignore"
     -> true
   | _ -> false

1006
(** Generate the top-level Coq declarations associated with
1007 1008 1009 1010
    a top-level declaration from a module.

    If a toplevel definition begins with [ignore "CFML"] in its body,
    then the toplevel definition is ignored by CFML altogether. *)
charguer's avatar
charguer committed
1011

1012
let rec cfg_structure_item s : cftops =
charguer's avatar
charguer committed
1013
  let loc = s.str_loc in
charguer's avatar
charguer committed
1014 1015 1016 1017
  match s.str_desc with
  | Tstr_value(rf, fvs, pat_expr_list) ->
      reset_local_labels();

1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069
      if List.exists is_ignored_str_value pat_expr_list then [] (* ignore *) else begin

        (* --todo: improve code sharing between local bindings and top-level bindings *)
        let is_let_fun (pat,exp) =
           match exp.exp_desc with
           | Texp_function (_,_,_) -> true
           | Texp_constraint({exp_desc = Texp_function (_,_,_)},_,_) -> true
           | _ -> false in

        if List.for_all is_let_fun pat_expr_list then begin
          let env' = match rf with
             | Nonrecursive -> Ident.empty
             | Recursive -> Ident.empty
                 (* --todo: better support for polymorphic recursion
                List.fold_left (fun (pat,bod) acc -> Ident.add (pattern_ident pat) 0 acc) env pat_expr_list *)
             | Default -> unsupported loc "Default recursion mode"
             in
          let ncs = List.map (fun (pat,bod) -> (pattern_name_protect_infix pat, cfg_func env' fvs pat bod)) pat_expr_list in
            (List.map (fun (name,_) -> Cftop_val (name, func_type)) ncs)
          @ (List.map (fun (name,cf_body) -> Cftop_fun_cf (name, cf_body)) ncs)
          @ [Cftop_coqs (List.map (fun (name,_) -> register_cf name) ncs)]

        (* let-binding of a single value *)
        end else if (List.length pat_expr_list = 1) then begin (* later: check it is not a function *)
          let (pat,bod) = List.hd pat_expr_list in
          let x = pattern_name_protect_infix pat in
          (* DEPRECATED if (hack_recognize_okasaki_lazy x) then [] else *)
          begin

          (* deprecated: pure-mode let-binding
          if !pure_mode then begin

             let cf_body = cfg_exp (Ident.empty) bod in
             let implicits =
                match fvs_strict with
                | [] -> []
                | _ ->  [ Coqtop_implicit (x, List.map (fun t -> (t,Coqi_maximal)) fvs_strict) ]
                in
             [ Cftop_val (x, coq_forall_types fvs_strict typ);
               Cftop_coqs implicits;
               Cftop_pure_cf (x, fvs_strict, fvs_others, cf_body);
               Cftop_coqs [register_cf x]; ]
          end else*)

          (* value let-binding *)
          if Typecore.is_nonexpansive bod then begin

             let v =
               try lift_val (Ident.empty) bod
               with Not_in_normal_form (loc2, s) ->
                  (* TODO: here and elsewhere, use a wrapper for extending the errors *)
                  raise (Not_in_normal_form (loc2, s ^ " (only value can satisfy the value restriction)"))
charguer's avatar
charguer committed
1070 1071
              in

1072 1073 1074 1075 1076 1077
             let fvs_typ, typ = lift_typ_sch loc pat.pat_type in
             let fvs = List.map name_of_type_var (List.filter typvar_is_used fvs) in
             if not (list_is_included fvs_typ fvs)
               then failwith "fvs_typ not included in fvs for let binding";
             let fvs_strict = fvs_typ in
             let fvs_others = list_minus fvs fvs_strict in
1078

1079 1080 1081 1082 1083 1084 1085 1086 1087 1088
             let v_typed = coq_annot v typ in
             let implicits =
                match fvs_strict with
                | [] -> []
                | _ ->  [ Coqtop_implicit (x, List.map (fun t -> (t,Coqi_maximal)) fvs_strict) ]
                in
             [ Cftop_val (x, coq_forall_types fvs_strict typ);
               Cftop_coqs implicits;
               Cftop_val_cf (x, fvs_strict, fvs_others, v_typed);
               Cftop_coqs [register_cf x]; ]
charguer's avatar
charguer committed
1089

1090 1091
          (* term let-binding -- later *)
          end else begin
1092

1093 1094
             unsupported loc "top-level binding of terms that are not values";
             (* let (fvs_strict, fvs_others, typ) = get_fvs_typ loc fvs pat.pat_type in*)
charguer's avatar
charguer committed
1095

1096 1097 1098 1099 1100 1101 1102 1103
             (* if fvs_strict <> [] || fvs_others <> []
                 then not_in_normal_form loc ("(unsatisfied value restriction) "
                                          ^ (Print_tast.string_of_expression false e));
             let cf1 = cfg_exp env bod in
             let env' = Ident.add (pattern_ident pat) (List.length fvs_strict) env in
             let cf2 = cfg_exp env' body in
             add_used_label x;
             Cf_let ((x,typ), cf1, cf2) *)
charguer's avatar
charguer committed
1104

1105
          end
charguer's avatar
charguer committed
1106

1107
        end (* for skip_cf *)
charguer's avatar
charguer committed
1108

1109 1110
       end else
          unsupported loc ("mutually-recursive values that are not all functions");
charguer's avatar
charguer committed
1111

1112
     end (* for ignored toplevel item *)
charguer's avatar
charguer committed
1113

charguer's avatar
charguer committed
1114
  | Tstr_type(decls) -> [ Cftop_coqs (cfg_type_decls loc decls) ]
charguer's avatar
charguer committed
1115

1116
  | Tstr_module(id, modl) -> cfg_module id modl
charguer's avatar
charguer committed
1117 1118 1119

  | Tstr_modtype(id, decl) -> cfg_modtype id decl

1120
  | Tstr_open path ->
charguer's avatar
charguer committed
1121
      (* TEMPORARILY DEPRECATED if is_primitive_module (Path.name path) then [] else *)
charguer's avatar
charguer committed
1122
      [ Cftop_coqs [ Coqtop_require_import [ lift_full_path_name path ] ] ]
charguer's avatar
charguer committed
1123 1124

  | Tstr_primitive(id, descr) ->
charguer's avatar
charguer committed
1125
      let id = var_name (Ident.name id) in
charguer's avatar
charguer committed
1126
      let fvs, typ = lift_typ_sch loc descr.val_desc.ctyp_type in
charguer's avatar
charguer committed
1127 1128 1129
      let typ = coq_fun_types fvs typ in
      [ Cftop_val (id, typ) ]

charguer's avatar
charguer committed
1130
  | Tstr_exception(id, decl) ->
1131
      [] (* unsupported "exceptions" ; could be raise CFML_ignore *)
1132
  | Tstr_exn_rebind(id, path) ->
1133
      [] (* unsupported "exceptions" ; could be raise CFML_ignore *)
charguer's avatar
charguer committed
1134

charguer's avatar
charguer committed
1135 1136 1137 1138 1139
  | Tstr_recmodule bindings -> unsupported loc "recursive modules"
  | Tstr_class _ -> unsupported loc "objects"
  | Tstr_class_type _ -> unsupported loc "objects"
  | Tstr_include (m,ids) -> unsupported loc "module-include"
  | Tstr_eval expr -> unsupported loc "top level eval expression (let _)"
charguer's avatar
charguer committed
1140

1141
(** Generate the top-level Coq declarations associated with
charguer's avatar
charguer committed
1142 1143 1144
    a type abbreviation. *)

and cfg_type_abbrev (name,dec) =
charguer's avatar
charguer committed
1145 1146 1147 1148
   let loc = dec.typ_loc in
   let x = Ident.name name in
   check_type_constr_name loc x;
   let name = type_constr_name x in
charguer's avatar
charguer committed
1149
   let args = List.map name_of_type_var dec.typ_type.type_params in
charguer's avatar
charguer committed
1150 1151
   let sort = coq_impl_types (List.length args) in
   let coqs = match dec.typ_type.type_manifest with
charguer's avatar
charguer committed
1152
      | None -> [Coqtop_param (name, sort)]
charguer's avatar
charguer committed
1153
      | Some t -> [Coqtop_def ((name, sort), coq_fun_types args (lift_typ_exp loc t));
charguer's avatar
charguer committed
1154
                   Coqtop_hint_unfold ([name],"typeclass_instances") ] in
charguer's avatar
charguer committed
1155
   coqs
charguer's avatar
charguer committed
1156

1157
(** Generate the top-level Coq declarations associated with
charguer's avatar
charguer committed
1158 1159 1160
    a record definition. *)

and cfg_type_record (name,dec) =
charguer's avatar
charguer committed
1161
   let loc = dec.typ_loc in
charguer's avatar
charguer committed
1162
   let x = Ident.name name in
charguer's avatar
charguer committed
1163
   check_type_constr_name loc x;
1164
   let name_of_field lbl =
charguer's avatar
charguer committed
1165
      record_field_name lbl in
charguer's avatar
charguer committed
1166 1167
   let fields = match dec.typ_type.type_kind with Type_record (l,_) -> l | _ -> assert false in
   (* let fields_base_names = List.map (fun (lbl,_,_) -> lbl) fields in *)
charguer's avatar
charguer committed
1168
   let declared_params = List.map name_of_type_var dec.typ_type.type_params in
1169 1170
   let branches, branches_params = List.split (List.map (fun (lbl, mut, typ) ->
      let btyp = btyp_of_typ_exp typ in
charguer's avatar
charguer committed
1171
      ((name_of_field lbl, lift_btyp loc btyp), fv_btyp ~through_arrow:false btyp)) fields) in
charguer's avatar
charguer committed
1172 1173 1174 1175 1176 1177
          (* todo: use a function to factorize above work *)

   (* deprecated sorting: let branches = list_ksort str_cmp branches in *)
   let fields_names, fields_types = List.split branches in
   (* let remaining_params = List.concat branches_params in *)
   (* todo: assert remaining_params included in declared_params *)
1178 1179 1180
   (* TODO: enlever le polymorphisme inutile : list_intersect remaining_params declared_params *)
   let params = declared_params in
   let _top = {
charguer's avatar
charguer committed
1181 1182
      coqind_name = record_structure_name x;
      coqind_constructor_name = record_constructor_name x;
charguer's avatar
charguer committed
1183 1184 1185
      coqind_targs = coq_types params;
      coqind_ret = Coq_type;
      coqind_branches = branches } in
charguer's avatar
charguer committed
1186
   let _implicit_decl =
charguer's avatar
charguer committed
1187 1188
      match params with
      | [] -> []
1189
      | _ -> List.map (fun field -> Coqtop_implicit (field, List.map (fun p -> p, Coqi_maximal) params)) fields_names
charguer's avatar
charguer committed
1190
      in
charguer's avatar
charguer committed
1191
   let type_abbrev = Coqtop_def ((type_constr_name x, Coq_wild), coq_fun_types params loc_type) in
charguer's avatar
charguer committed
1192
   [ type_abbrev ] @
charguer's avatar
charguer committed
1193
   (* DEPRECATED BUT KEEP FOR FUTURE USE
1194
   [ Coqtop_record top ]
charguer's avatar
charguer committed
1195
   @ (implicit_decl)
charguer's avatar
charguer committed
1196
   @ [ Coqtop_hint_constructors ([record_structure_name x], "typeclass_instances") ]
1197
   @
charguer's avatar
charguer committed
1198 1199
   *)
   record_functions x (record_constructor_name x) (record_repr_name x) params fields_names fields_types
charguer's avatar
charguer committed
1200 1201 1202 1203
  (*  todo: move le "_of" *)

(** Auxiliary function to generate stuff for records *)

1204
and record_functions name record_constr repr_name params fields_names fields_types =
charguer's avatar
charguer committed
1205
   let build_field_name_def i field_name =
1206
      Coqtop_def ((field_name, coq_nat), Coq_nat i)
charguer's avatar
charguer committed
1207 1208 1209 1210 1211
      in
   let fields_names_def = list_mapi build_field_name_def fields_names in
   fields_names_def

   (* DEPRECATED BUT KEEP FOR FUTURE USE
charguer's avatar
charguer committed
1212 1213 1214 1215 1216
   let nth i l = List.nth l i in
   let n = List.length fields_names in
   let indices = list_nat n in
   let for_indices f = List.map f indices in

charguer's avatar
charguer committed
1217
   let new_name = record_make_name name in
charguer's avatar
charguer committed
1218 1219
   let get_names = for_indices (fun i -> record_field_get_name (nth i fields_names)) in
   let set_names = for_indices (fun i -> record_field_set_name (nth i fields_names)) in
charguer's avatar
charguer committed
1220
   let new_decl = Coqtop_param (new_name, func_type) in
charguer's avatar
charguer committed
1221
   let get_set_decl i =
1222
      [ Coqtop_param (nth i get_names, func_type);
charguer's avatar
charguer committed
1223
        Coqtop_param (nth i set_names, func_type) ] in
1224

charguer's avatar
charguer committed
1225
   let logicals = List.map str_capitalize_1 fields_names in
charguer's avatar
charguer committed
1226 1227 1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243 1244
   let reprs = for_indices (fun i -> sprintf "_T%d" (i+1)) in
   let abstracts = for_indices (fun i -> sprintf "_X%d" (i+1)) in
   let concretes = for_indices (fun i -> sprintf "x%d" (i+1)) in
   let loc = "l" in

   let vparams = coq_vars params in
   let vlogicals = coq_vars logicals in
   let vreprs = coq_vars reprs in
   let vabstracts = coq_vars abstracts in
   let vconcretes = coq_vars concretes in
   let vloc = coq_var "l" in

   let tparams = coq_types params in
   let tlogicals = coq_types logicals in
   let treprs = List.map (fun i -> nth i reprs, htype (nth i vlogicals) (nth i fields_types)) indices in
   let tabstracts = List.map (fun i -> nth i abstracts, nth i vlogicals) indices in
   let tconcretes = List.map (fun i -> nth i concretes, nth i fields_types) indices in
   let tloc = (loc, loc_type) in

charguer's avatar
charguer committed
1245

charguer's avatar
charguer committed
1246 1247 1248 1249 1250 1251 1252 1253 1254 1255 1256 1257 1258 1259 1260 1261
   let repr_args = tparams @ tlogicals @ treprs @ tabstracts @ [tloc] in
   let hcore = heap_is_single vloc (coq_apps (coq_var_at record_constr) (vparams @ vconcretes)) in
   let helems_items = for_indices (fun i -> hdata (nth i vconcretes) (Coq_app (nth i vreprs, nth i vabstracts))) in
   let helems = heap_stars helems_items in
   let repr_body = heap_star hcore helems in
   let repr_def = coqtop_def_untyped repr_name (coq_funs repr_args (heap_existss tconcretes repr_body)) in

   let repr_folded = hdata vloc (coq_apps (coq_var_at repr_name) (vparams @ vlogicals @ vreprs @ vabstracts)) in
   let repr_unfolded = hdata vloc (coq_apps (coq_var_at repr_name) (vparams @ fields_types @ (list_make n id_repr) @ vconcretes)) in
   let repr_elems = helems in
   let repr_convert_body = coq_eq repr_folded (heap_existss tconcretes (heap_star repr_unfolded repr_elems)) in
   let repr_focus_body = heap_impl repr_folded (heap_existss tconcretes (heap_star repr_unfolded repr_elems)) in
   let repr_unfocus_body = heap_impl (heap_star repr_unfolded repr_elems) repr_folded in
   let repr_convert_quantif = [tloc] @ tparams @ tlogicals @ treprs @ tabstracts in
   let repr_focus_quantif = repr_convert_quantif in
   let repr_unfocus_quantif = [tloc] @ tparams @ tconcretes @ tlogicals @ treprs @ tabstracts in
charguer's avatar
charguer committed
1262 1263 1264
   let convert_name = record_convert_name name in
   let focus_name = record_unfocus_name name in
   let unfocus_name = record_focus_name name in
charguer's avatar
charguer committed
1265 1266
   let repr_convert = Coqtop_param (convert_name, coq_foralls repr_convert_quantif repr_convert_body) in
   let repr_focus = Coqtop_param (focus_name, coq_foralls repr_focus_quantif repr_focus_body) in