Commit 2c287e3c authored by charguer's avatar charguer

primitives

parent 41a5ef66
......@@ -3,8 +3,34 @@
URGENT
SANITY
- reject programs with constructor names ending with "_"
(e.g. "A_" is already used for type variables *)
- reject variable names and type definition that belongs to the list
builtin_type_constructors
- rename on the fly coq keyword such as exists, forall, etc..
=> requires a list of all coq keywords: see
else if name = "exists" then "exists__"
else if name = "forall" then "forall__"
- restriction on not binding "min" and "max" could be a bit restrictive..
LATER
- in print_tast and print_past, protect with parenth the infix names being bound
- make sure that check_var is called where needed
- need to prevent double-underscore in the names?
- unify the source code in main.ml and makecmj.ml
- check that there are no uses of labels in source files
......@@ -16,4 +42,15 @@ DEPRECATED?
- no longer rely on myocamldep
- incorrect CF generation for "let n = null"
\ No newline at end of file
- incorrect CF generation for "let n = null"
(*
(** Auxiliary function for the special case of compiling pervasives *)
let add_pervasives_prefix_if_needed p =
if !Clflags.nopervasives then "Pervasives." ^ p else p
let p = add_pervasives_prefix_if_needed p in
*)
\ No newline at end of file
......@@ -5,13 +5,34 @@ Require Import Demo_ml.
Require Import Pervasives_ml. (* optional, improves display of, e.g. [incr] *)
(*Open Scope tag_scope.*)
Print TLC.LibOrder.ge_from_le.
Definition f := (fun x_ y_ : int => TLC.LibReflect.isTrue (x_ >= y_)).
Print f.
Definition g := .
(fun x_ y_ : int => TLC.LibReflect.isTrue (TLC.LibOrder.lt (TLC.LibOrder.ge_from_le TLC.LibInt.le) x_ y_)).
"Pervasives.<=", (Primitive_binary_only_numbers, "(fun x_ y_ : int => TLC.LibReflect.isTrue (@TLC.LibOrder.le int TLC.LibInt.le_int_inst x_ y_))");
"Pervasives.>", (Primitive_binary_only_numbers, "(fun x_ y_ : int => TLC.LibReflect.isTrue (@TLC.LibOrder.gt int (TLC.LibOrder.gt_from_le TLC.LibInt.le_int_inst) x_ y_))");
"Pervasives.>=", (Primitive_binary_only_numbers, "(fun x_ y_ : int => TLC.LibReflect.isTrue (@TLC.LibOrder.ge int (TLC.LibOrder.ge_from_le TLC.LibInt.le_int_inst) x_ y_))");
Print f.
Locate ge_from_le.
Locate le_int_inst.
Definition g :=
(fun x_ y_ : int => TLC.LibReflect.isTrue (x_ <> y_))..
Print g.
Locate le_int_inst.
(*Open Scope tag_scope.*)
......
This diff is collapsed.
......@@ -88,3 +88,5 @@ val cfg_module : Ident.t -> Typedtree.module_expr -> Formula.cftops
*)
val cfg_file : Typedtree.structure -> Formula.cftop list
exception Not_in_normal_form of Location.t * string
......@@ -246,7 +246,7 @@ let rec coqtops_of_imp_cf cf =
*)
| Cf_manual c -> c
| Cf_letpure _ -> unsupported "letpure-expression in imperative mode"
| Cf_letpure _ -> unsupported_noloc "letpure-expression in imperative mode"
(* --todo: scope of type variables should be different than that of program variables: prefix them! *)
......
......@@ -93,9 +93,6 @@ let _ =
with _ -> Printf.printf "Could not create debug directory\n" end;
(*---------------------------------------------------*)
if sourcefile = "imper/MyLib.ml" then exit 0;
(*---------------------------------------------------*)
trace "2) reading and typing source file";
let (opt,inputfile) = process_implementation_file ppf sourcefile in
......@@ -114,11 +111,15 @@ let _ =
(*---------------------------------------------------*)
trace "4) typing normalized code";
let (typedtree2, _ : Typedtree.structure * Typedtree.module_coercion) =
match typecheck_implementation_file ppf sourcefile parsetree2 with
| None -> failwith "Could not typecheck the normalized source code\nCheck out the file output/_normalized.ml."
| Some typedtree2 -> typedtree2
in
let fail () =
failwith (Printf.sprintf "Could not typecheck the normalized source code\nCheck out the file %s_normalized.ml." debugdirBase) in
try
match typecheck_implementation_file ppf sourcefile parsetree2 with
| None -> fail() (* TODO: useful?*)
| Some typedtree2 -> typedtree2
with Typetexp.Error(loc, err) -> fail()
in
(*---------------------------------------------------*)
trace "5) dumping .cmj file";
file_put_contents (debugdirBase ^ "_normalized_typed.ml") (Print_tast.string_of_structure typedtree2);
......@@ -132,7 +133,15 @@ let _ =
(*---------------------------------------------------*)
trace "5) constructing caracteristic formula ast";
let cftops = Characteristic.cfg_file typedtree2 in
let cftops =
try Characteristic.cfg_file typedtree2
with
| Typetexp.Error(_, _) -> assert false
| Characteristic.Not_in_normal_form (loc, s) ->
Location.print_error Format.std_formatter loc;
Printf.printf " %s.\nThe normalized file does not appear to be in normal form.\nTo investigate, open %s_normalized.ml\nand %s_normalized_typed.ml.\n" s debugdirBase debugdirBase;
exit 1
in
(*---------------------------------------------------*)
trace "6) converting caracteristic formula ast to coq ast";
......
......@@ -210,9 +210,15 @@ let show_str s =
let output s =
Printf.printf "%s\n" s
let warning s =
let warning s = (* DEPRECATED? *)
Printf.printf "### WARNING: %s\n" s
let unsupported s =
failwith ("Unsupported language construction : " ^ s)
let unsupported_noloc s =
failwith ("Unsupported language construction : " ^ s)
let unsupported loc s =
Location.print_error Format.err_formatter loc;
unsupported_noloc s
(* TODO: report location *)
......@@ -124,4 +124,9 @@ val warning : string -> unit
(** Display a message explaining that a feature is not supported *)
val unsupported : string -> 'a
val unsupported_noloc : string -> 'a
(** Display a message explaining that a feature is not supported,
and report the location *)
val unsupported : Location.t -> string -> 'a
This diff is collapsed.
......@@ -11,21 +11,24 @@ open Format
(*#########################################################################*)
(* ** Printing of base values *)
let parent_if_infix s =
if Renaming.is_infix_name s then sprintf "(%s)" s else s
let string_of_ident s =
Ident.name s
parent_if_infix (Ident.name s)
let string_of_lident idt =
let names = Longident.flatten idt in
String.concat "." names
parent_if_infix (String.concat "." names)
let string_of_constant = function
| Const_int n -> string_of_int n
| Const_char c -> String.make 1 c
| Const_string s -> s
| Const_float f -> f
| Const_int32 _ -> unsupported "int32 type"
| Const_int64 _ -> unsupported "int64 type"
| Const_nativeint _ -> unsupported "native int type"
| Const_int32 _ -> unsupported_noloc "int32 type"
| Const_int64 _ -> unsupported_noloc "int64 type"
| Const_nativeint _ -> unsupported_noloc "native int type"
let string_of_recflag = function
| Nonrecursive -> ""
......@@ -48,21 +51,21 @@ let string_of_pattern par p =
| Ppat_tuple l ->
show_par true (sprintf "%s" (show_list (aux false) "," l))
| Ppat_construct (li, po, b) ->
if (b != false) then unsupported "construct with options";
if (b != false) then unsupported_noloc "construct with options";
let s = sprintf "%s%s"
(string_of_lident li)
(show_option (aux true) po) in
show_par par s
| Ppat_lazy p1 ->
show_par par (sprintf "lazy %s" (aux true p1))
| Ppat_variant (_,_) -> unsupported "variant patterns"
| Ppat_record _ -> unsupported "record patterns"
| Ppat_array pats -> unsupported "array patterns"
| Ppat_variant (_,_) -> unsupported_noloc "variant patterns"
| Ppat_record _ -> unsupported_noloc "record patterns"
| Ppat_array pats -> unsupported_noloc "array patterns"
| Ppat_or (p1,p2) ->
show_par par (sprintf "%s | %s" (aux false p1) (aux false p2))
| Ppat_constraint (p,t) -> sprintf "(%s : _)" (aux false p)
| Ppat_type t -> unsupported "type patterns"
| Ppat_unpack _ -> unsupported "pat_unpack"
| Ppat_type t -> unsupported_noloc "type patterns"
| Ppat_unpack _ -> unsupported_noloc "pat_unpack"
in
aux false p
......@@ -100,7 +103,7 @@ let rec string_of_expression par e =
show_par par s
| Pexp_function (p1, None, l) ->
Format.sprintf "@[function %s@]" (show_listp string_of_branch "\n | " l)
| Pexp_function (p, Some _, l) -> unsupported "function with optional expression"
| Pexp_function (p, Some _, l) -> unsupported_noloc "function with optional expression"
| Pexp_apply (e, l) -> (* todo: afficher les infixes correctement *)
let s = (aux ~par:true e) ^ " " ^ (show_list (aux ~par:true) " " (List.map snd l)) in
show_par par s
......@@ -108,17 +111,17 @@ let rec string_of_expression par e =
let s = Format.sprintf "@[match@ @[%s@] with@ @[%s@]@]"
(aux e) (show_list string_of_branch " | " l) in
show_par par s
| Pexp_try (e,l) -> unsupported "exceptions"
| Pexp_try (e,l) -> unsupported_noloc "exceptions"
| Pexp_tuple l ->
show_par true (show_list aux ", " l)
| Pexp_construct (li, eo, b) ->
if (b != false)
then unsupported "data constructor with option";
then unsupported_noloc "data constructor with option";
let s = Format.sprintf "@[%s%s@]" (string_of_lident li)
(show_option (aux ~par:true) eo) in
show_par par s
| Pexp_variant (l,eo) -> unsupported "variants"
| Pexp_record (l,Some eo) -> unsupported "record-with"
| Pexp_variant (l,eo) -> unsupported_noloc "variants"
| Pexp_record (l,Some eo) -> unsupported_noloc "record-with"
| Pexp_record (l,None) ->
let print_item (li,ei) =
Format.sprintf "%s = %s" (string_of_lident li) (aux ei) in
......@@ -130,7 +133,7 @@ let rec string_of_expression par e =
| Pexp_setfield (e,i,e2) ->
let s = Format.sprintf "@[%s.%s <- %s@]" (aux e) (string_of_lident i) (aux e2) in
show_par par s
| Pexp_array l -> unsupported "array expression" (* Pexp_array (List.map aux l)*)
| Pexp_array l -> unsupported_noloc "array expression" (* Pexp_array (List.map aux l)*)
| Pexp_ifthenelse (e1, e2, None) ->
let s = Format.sprintf "@[if %s@ then %s@]" (aux e1) (aux e2) in
show_par par s
......@@ -151,11 +154,11 @@ let rec string_of_expression par e =
show_par par s
| Pexp_when (e1,e2) -> (*todo:better printing so that compiles *)
Format.sprintf "<< when %s >> %s" (aux e1) (aux e2)
| Pexp_send (_,_) -> unsupported "send expression"
| Pexp_new _ -> unsupported "new expression"
| Pexp_setinstvar (_,_) -> unsupported "set-inst-var expression"
| Pexp_override _ -> unsupported "Pexp_override expression"
| Pexp_letmodule (_,_,_) -> unsupported "let-module expression"
| Pexp_send (_,_) -> unsupported_noloc "send expression"
| Pexp_new _ -> unsupported_noloc "new expression"
| Pexp_setinstvar (_,_) -> unsupported_noloc "set-inst-var expression"
| Pexp_override _ -> unsupported_noloc "Pexp_override expression"
| Pexp_letmodule (_,_,_) -> unsupported_noloc "let-module expression"
| Pexp_assert e ->
let s = Format.sprintf "@[assert %s@]" (aux e) in
show_par par s
......@@ -164,11 +167,11 @@ let rec string_of_expression par e =
| Pexp_lazy e ->
let s = Format.sprintf "@[lazy %s@]" (aux e) in
show_par par s
| Pexp_poly (_,_) -> unsupported "poly expression"
| Pexp_object _ -> unsupported "objects"
| Pexp_open _ -> unsupported "open in"
| Pexp_pack _ -> unsupported "pack"
| Pexp_newtype _ -> unsupported "new type"
| Pexp_poly (_,_) -> unsupported_noloc "poly expression"
| Pexp_object _ -> unsupported_noloc "objects"
| Pexp_open _ -> unsupported_noloc "open in"
| Pexp_pack _ -> unsupported_noloc "pack"
| Pexp_newtype _ -> unsupported_noloc "new type"
(*#########################################################################*)
(* ** Normalization of modules and top-level phrases *)
......@@ -180,7 +183,7 @@ let rec string_of_module m =
| Pmod_functor (s,mt,me) -> sprintf "%s : _ ==>%s\n" s (string_of_module me)
| Pmod_apply (me1,me2) -> sprintf "%s %s" (string_of_module me1) (string_of_module me2)
| Pmod_constraint (me,mt) -> sprintf "(%s : _)" (string_of_module me)
| Pmod_unpack _ -> unsupported "unpack"
| Pmod_unpack _ -> unsupported_noloc "unpack"
and string_of_structure s =
show_list string_of_structure_item lin2 s
......@@ -195,16 +198,16 @@ and string_of_structure_item si =
Format.sprintf "%s =@ @[%s@]" sp se in
let sl = show_list show_pe " and " l in
Format.sprintf "@[let%s %s@]" (string_of_recflag r) sl
| Pstr_primitive (s,v) -> sprintf "val %s : _" s
| Pstr_primitive (s,v) -> sprintf "val %s : 'external" s
| Pstr_type l -> sprintf "type _ = _"
| Pstr_exception (s,e) -> sprintf "exception %s = _" s
| Pstr_exn_rebind (s,i) -> unsupported "exception-rebind"
| Pstr_exn_rebind (s,i) -> unsupported_noloc "exception-rebind"
| Pstr_module (s,m) -> Format.sprintf "@[module %s =@ @[<2>%s] @]" s (string_of_module m)
| Pstr_recmodule _ -> unsupported "recursive modules"
| Pstr_recmodule _ -> unsupported_noloc "recursive modules"
| Pstr_modtype (s,mt) -> sprintf "module type %s = _" s
| Pstr_open li -> sprintf "open %s = _" (string_of_lident li)
| Pstr_class _ -> unsupported "objects"
| Pstr_class_type _ -> unsupported "objects"
| Pstr_class _ -> unsupported_noloc "objects"
| Pstr_class_type _ -> unsupported_noloc "objects"
| Pstr_include m -> sprintf "include %s" (string_of_module m)
and string_of_toplevel_phrase p =
......
......@@ -51,9 +51,9 @@ let string_of_pattern par p =
show_par par (sprintf "%s | %s" (aux false p1) (aux false p2))
| Tpat_lazy p1 ->
show_par par (sprintf "lazy %s" (aux true p1))
| Tpat_variant (_,_,_) -> unsupported "variant patterns"
| Tpat_record _ -> unsupported "record patterns"
| Tpat_array pats -> unsupported "array patterns"
| Tpat_variant (_,_,_) -> unsupported_noloc "variant patterns"
| Tpat_record _ -> unsupported_noloc "record patterns"
| Tpat_array pats -> unsupported_noloc "array patterns"
in
aux false p
......@@ -66,7 +66,7 @@ let string_of_let_pattern par fvs p =
| Tpat_var id ->
let typ = p.pat_type in
sprintf "%s : %s" (string_of_ident id) (string_of_type_sch fvs typ)
| _ -> unsupported "let-pattern not reduced to a variable"
| _ -> unsupported_noloc "let-pattern not reduced to a variable"
*)
(*#########################################################################*)
......@@ -106,7 +106,7 @@ let rec string_of_expression par e =
| Texp_function (_,l, pa) ->
Format.sprintf "@[function %s@]" (show_listp string_of_branch "\n | " l)
| Texp_apply (e, l) -> (* todo: afficher les infixes correctement *)
let l = List.map (fun (lab,eo,opt) -> match eo with None -> unsupported "optional apply arguments" | Some ei -> ei) l in
let l = List.map (fun (lab,eo,opt) -> match eo with None -> unsupported_noloc "optional apply arguments" | Some ei -> ei) l in
let se = aux ~par:true e in
let show_arg ei =
let s_ei = aux ~par:false ei in
......@@ -120,7 +120,7 @@ let rec string_of_expression par e =
let s = Format.sprintf "@[match@ @[%s@] with@ @[%s@]@]"
se (show_list string_of_branch " | " l) in
show_par par s
| Texp_try (e,l) -> unsupported "exceptions"
| Texp_try (e,l) -> unsupported_noloc "exceptions"
| Texp_tuple l ->
show_par true (show_list aux ", " l)
| Texp_construct (p, cd, es) ->
......@@ -131,8 +131,8 @@ let rec string_of_expression par e =
then show_par par (c ^ " " ^ aux ~par:true (List.hd es))
else
show_par par (sprintf "%s (%s)" c (show_list aux "," es))
| Texp_variant (l,eo) -> unsupported "variants"
| Texp_record (l,Some eo) -> unsupported "record-with"
| Texp_variant (l,eo) -> unsupported_noloc "variants"
| Texp_record (l,Some eo) -> unsupported_noloc "record-with"
| Texp_record (l,None) ->
let print_item (p,li,ei) =
Format.sprintf "%s = %s" (string_of_path p) (aux ei) in
......@@ -144,7 +144,7 @@ let rec string_of_expression par e =
| Texp_setfield (e,p,i,e2) ->
let s = Format.sprintf "@[%s.%s <- %s@]" (aux e) (string_of_path p) (aux e2) in
show_par par s
| Texp_array l -> unsupported "array expression" (* Texp_array (List.map aux l)*)
| Texp_array l -> unsupported_noloc "array expression" (* Texp_array (List.map aux l)*)
| Texp_ifthenelse (e1, e2, None) ->
let s = Format.sprintf "@[if %s@ then %s@]" (aux e1) (aux e2) in
show_par par s
......@@ -162,12 +162,12 @@ let rec string_of_expression par e =
| Texp_for (i,e1,e2,d,e3) ->
let s = Format.sprintf "@[for %s = %s to %s do@ %s@ done@]" (Ident.name i) (aux e1) (aux e2) (aux e3) in
show_par par s
| Texp_send (_,_,_) -> unsupported "send expression"
| Texp_new _ -> unsupported "new expression"
| Texp_instvar (_,_) -> unsupported "inst-var expression"
| Texp_setinstvar (_,_,_) -> unsupported "set-inst-var expression"
| Texp_override _ -> unsupported "Pexp_override expression"
| Texp_letmodule (_,_,_) -> unsupported "let-module expression"
| Texp_send (_,_,_) -> unsupported_noloc "send expression"
| Texp_new _ -> unsupported_noloc "new expression"
| Texp_instvar (_,_) -> unsupported_noloc "inst-var expression"
| Texp_setinstvar (_,_,_) -> unsupported_noloc "set-inst-var expression"
| Texp_override _ -> unsupported_noloc "Pexp_override expression"
| Texp_letmodule (_,_,_) -> unsupported_noloc "let-module expression"
| Texp_assert e ->
let s = Format.sprintf "@[assert %s@]" (aux e) in
show_par par s
......@@ -176,11 +176,11 @@ let rec string_of_expression par e =
| Texp_lazy e ->
let s = Format.sprintf "@[lazy %s@]" (aux e) in
show_par par s
| Texp_object _ -> unsupported "objects"
| Texp_poly (_,_) -> unsupported "poly"
| Texp_newtype (_,_) -> unsupported "newtype"
| Texp_pack _ -> unsupported "pack"
| Texp_open (_,_) -> unsupported "open"
| Texp_object _ -> unsupported_noloc "objects"
| Texp_poly (_,_) -> unsupported_noloc "poly"
| Texp_newtype (_,_) -> unsupported_noloc "newtype"
| Texp_pack _ -> unsupported_noloc "pack"
| Texp_open (_,_) -> unsupported_noloc "open"
| Texp_constraint (e,_,_) -> aux e
......@@ -203,12 +203,12 @@ let show_core_type par t =
| l -> show_par true (show_list (aux false) ", " l)
in
sprintf "%s %s" args (string_of_path p)
| Ttyp_object _ -> unsupported "object types"
| Ttyp_class _ -> unsupported "class types"
| Ttyp_alias _ -> unsupported "alias types"
| Ttyp_variant _ -> unsupported "variant types"
| Ttyp_poly _ -> unsupported "poly types"
| Ttyp_package _ -> unsupported "package types"
| Ttyp_object _ -> unsupported_noloc "object types"
| Ttyp_class _ -> unsupported_noloc "class types"
| Ttyp_alias _ -> unsupported_noloc "alias types"
| Ttyp_variant _ -> unsupported_noloc "variant types"
| Ttyp_poly _ -> unsupported_noloc "poly types"
| Ttyp_package _ -> unsupported_noloc "package types"
in
aux par t
......@@ -230,7 +230,7 @@ let show_type_decl (name,decl) =
| Some def -> sprintf "%s = %s" header (show_type def)
end
| Ttype_record _ (* (string * mutable_flag * core_type * Location.t) list *) ->
unsupported "records type def (todo)"
unsupported_noloc "records type def (todo)"
| Ttype_variant branches ->
let show_branch (constr, args, _) =
match args with
......@@ -258,7 +258,7 @@ let rec string_of_module m =
| Tmod_functor (id,mt,me) -> sprintf "%s : _ ==>%s\n" (string_of_ident id) (string_of_module me)
| Tmod_apply (me1,me2,mc) -> sprintf "%s %s" (string_of_module me1) (string_of_module me2)
| Tmod_constraint (me,_,mt,mc) -> sprintf "(%s : _)" (string_of_module me)
| Tmod_unpack (_,_) -> unsupported "unpack"
| Tmod_unpack (_,_) -> unsupported_noloc "unpack"
and string_of_structure (s:structure) =
show_list string_of_structure_item lin2 s.str_items
......@@ -275,14 +275,14 @@ and string_of_structure_item (si:structure_item) =
let sl = show_list show_pe " and " l in
Format.sprintf "@[let%s %s@]" (string_of_recflag r) sl
(* Format.sprintf "@[let%s %s =@ @[<2>%s@]@]" *)
| Tstr_primitive (id,v) -> sprintf "val %s : _" (string_of_ident id)
| Tstr_primitive (id,v) -> sprintf "val %s : 'external" (string_of_ident id)
| Tstr_type l -> sprintf "type _ = _"
| Tstr_exception (id,e) -> sprintf "exception %s = _" (string_of_ident id)
| Tstr_exn_rebind (id,p) -> unsupported "exception-rebind"
| Tstr_exn_rebind (id,p) -> unsupported_noloc "exception-rebind"
| Tstr_module (id,m) -> Format.sprintf "@[module %s =@ @[<2>%s] @]" (string_of_ident id) (string_of_module m)
| Tstr_recmodule _ -> unsupported "recursive modules"
| Tstr_recmodule _ -> unsupported_noloc "recursive modules"
| Tstr_modtype (id,mt) -> sprintf "module type %s = _" (string_of_ident id)
| Tstr_open p -> sprintf "open %s = _" (string_of_path p)
| Tstr_class _ -> unsupported "objects"
| Tstr_class_type _ -> unsupported "objects"
| Tstr_class _ -> unsupported_noloc "objects"
| Tstr_class_type _ -> unsupported_noloc "objects"
| Tstr_include (m,ids) -> sprintf "include %s" (string_of_module m)
......@@ -62,8 +62,8 @@ let mark_loops = mark_loops
let name_of_type ty =
let ty = proxy ty in
let x = name_of_type ty in
type_constr_name (String.uppercase x)
let x = Printtyp.name_of_type ty in
type_variable_name x
let reset_names = reset_names
......@@ -112,8 +112,8 @@ let rec btree_of_typexp sch ty =
Btyp_tuple (btree_of_typlist sch tyl)
| Tconstr(p, tyl, abbrev) ->
Btyp_constr (p, btree_of_typlist sch tyl)
| Tvariant row -> unsupported "variant"
| Tobject (fi, nm) -> unsupported "object"
| Tvariant row -> unsupported_noloc "variant"
| Tobject (fi, nm) -> unsupported_noloc "object"
| Tsubst ty ->
btree_of_typexp sch ty
| Tlink _ | Tnil | Tfield _ ->
......@@ -133,7 +133,7 @@ let rec btree_of_typexp sch ty =
| Tunivar ->
Btyp_var (false, name_of_type ty)
| Tpackage _ ->
unsupported "packaged types"
unsupported_noloc "packaged types"
in
if List.memq px !delayed then delayed := List.filter ((!=) px) !delayed;
if is_aliased px && aliasable ty then begin
......
......@@ -10,41 +10,34 @@ let check_var loc x =
as we use such an underscore to disambiguate with type variables *)
let n = String.length x in
if n > 0 && x.[n-1] = '_'
then unsupported ("variables names should not end with an underscore: " ^ x);
then unsupported loc ("variables names should not end with an underscore: " ^ x);
if (not !Clflags.nopervasives)
&& (List.mem x ["mod"; "/"; "&&"; "||"; "="; "<>"; "<="; ">="; "<"; ">"])
then unsupported ("CFML requires -nopervasives to allow binding of operator: " ^ x)
&& (List.mem x ["mod"; "/"; "&&"; "||"; "="; "<>"; "<="; ">="; "<"; ">"; "min"; "max"])
then unsupported loc ("CFML requires -nopervasives to allow binding of operator: " ^ x)
(* --is this line needed? if loc.loc_ghost then () else *)
(* TODO: also reject programs with variables that may clash with these! *)
(* TODO: make sure that check_var is called where needed *)
(* TODO: need to prevent double-underscore in the names? *)
(* TODO: should check that constructor names don't end with "_"
because these are used by type variables, e.g. "A_" *)
(* TODO: rename on the fly coq keyword such as exists, forall, etc...*)
(* should forbid all variables names that clash with a builtin type
from list "builtin_type_constructors", defined below *)
(*#########################################################################*)
(* ** Fresh name generation *)
(** Remark: we use a double underscore as suffix, to avoid clashes
with type constructors, which we make end with a single slash. *)
(** Fresh pattern variable name *)
let pattern_generated_name i =
"_p" ^ string_of_int i
"p" ^ string_of_int i ^ "__"
(** Fresh function variable name *)
let function_generated_name i =
"_f" ^ string_of_int i
"f" ^ string_of_int i ^ "__"
(** Fresh variable name *)
let variable_generated_name i =
"_x" ^ string_of_int i
"x" ^ string_of_int i ^ "__"
(*#########################################################################*)
......@@ -53,6 +46,12 @@ let variable_generated_name i =
let builtin_type_constructors =
[ "int"; "unit"; "bool"; "float"; "list"; "string"; "array"; "option" ]
(** Convention for naming type variables;
Here, the argument [name] is that provided by the OCaml type-checker. *)
let type_variable_name name =
(String.uppercase name) ^ "_"
(** Convention for naming type constructors *)
let type_constr_name name =
......@@ -90,7 +89,6 @@ let find_builtin_constructor p =
(*#########################################################################*)
(* ** List of inlined primitive functions *)
......@@ -104,14 +102,12 @@ let find_builtin_constructor p =
val primitive_special : int
*)
(* URGENT : support lazy operators! *)
(* URGENT : support comparison operators on base types! *)
type primitive_arity =
| Primitive_unary
| Primitive_binary
| Primitive_binary_lazy
| Primitive_binary_only_non_zero_second_arg
| Primitive_binary_div_or_mod
| Primitive_binary_only_numbers
let inlined_primitives_table =
......@@ -127,20 +123,21 @@ let inlined_primitives_table =
"Pervasives.snd", (Primitive_unary, "(@Coq.Init.Datatypes.snd _ _)");
"Pervasives.pred", (Primitive_unary, "CFML.CFHeader.pred");
"Pervasives.succ", (Primitive_unary, "CFML.CFHeader.succ");
"Pervasives./", (Primitive_binary_only_non_zero_second_arg, "CFML.CFHeader.int_div");
"Pervasives.mod", (Primitive_binary_only_non_zero_second_arg, "CFML.CFHeader.int_mod");
"Pervasives./", (Primitive_binary_div_or_mod, "CFML.CFHeader.int_div");
"Pervasives.mod", (Primitive_binary_div_or_mod, "CFML.CFHeader.int_mod");
"Pervasives.&&", (Primitive_binary_lazy, "TLC.LibBool.and");
"Pervasives.||", (Primitive_binary_lazy, "TLC.LibBool.or");
"Pervasives.=", (Primitive_binary_only_numbers, "(fun x_ y_ => TLC.LibReflect.isTrue (x_ = y_))");
"Pervasives.<>", (Primitive_binary_only_numbers, "(fun x_ y_ => TLC.LibReflect.isTrue (x_ <> y_))");
"Pervasives.<", (Primitive_binary_only_numbers, "(fun x_ y_ => TLC.LibReflect.isTrue (x_ < y_))");
"Pervasives.<=", (Primitive_binary_only_numbers, "(fun x_ y_ => TLC.LibReflect.isTrue (x_ <= y_))");
"Pervasives.>", (Primitive_binary_only_numbers, "(fun x_ y_ => TLC.LibReflect.isTrue (x_ > y_))");
"Pervasives.>=", (Primitive_binary_only_numbers, "(fun x_ y_ => TLC.LibReflect.isTrue (x_ >= y_))");
"Pervasives.=", (Primitive_binary_only_numbers, "(fun x_ y_ : int => TLC.LibReflect.isTrue (Coq.Init.Logic.eq x_ y_))");
"Pervasives.<>", (Primitive_binary_only_numbers, "(fun x_ y_ : int => TLC.LibReflect.isTrue (Coq.Init.Logic.not (Coq.Init.Logic.eq x_ y_)))");
"Pervasives.<", (Primitive_binary_only_numbers, "(fun x_ y_ : int => TLC.LibReflect.isTrue (@TLC.LibOrder.lt int (@TLC.LibOrder.lt_from_le int TLC.LibInt.le_int_inst) x_ y_))");
"Pervasives.<=", (Primitive_binary_only_numbers, "(fun x_ y_ : int => TLC.LibReflect.isTrue (@TLC.LibOrder.le int TLC.LibInt.le_int_inst x_ y_))");
"Pervasives.>", (Primitive_binary_only_numbers, "(fun x_ y_ : int => TLC.LibReflect.isTrue (@TLC.LibOrder.gt int (@TLC.LibOrder.gt_from_le int TLC.LibInt.le_int_inst) x_ y_))");
"Pervasives.>=", (Primitive_binary_only_numbers, "(fun x_ y_ : int => TLC.LibReflect.isTrue (@TLC.LibOrder.ge int (@TLC.LibOrder.ge_from_le int TLC.LibInt.le_int_inst) x_ y_))");
"Pervasives.max", (Primitive_binary_only_numbers, "Coq.ZArith.BinInt.Zmax");
"Pervasives.min", (Primitive_binary_only_numbers, "Coq.ZArith.BinInt.Zmin");
]