From 3cb32772ccd0f2882a40d7f75b044b738adadad3 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Tue, 22 Oct 2019 11:57:16 +0200 Subject: Add extraction for primitive floats Co-authored-by: Pierre Roux --- plugins/extraction/mlutil.ml | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) (limited to 'plugins/extraction/mlutil.ml') diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 000df26858..44b95ae4c1 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -398,6 +398,7 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with | MLaxiom, MLaxiom -> true | MLmagic t1, MLmagic t2 -> eq_ml_ast t1 t2 | MLuint i1, MLuint i2 -> Uint63.equal i1 i2 +| MLfloat f1, MLfloat f2 -> Float64.equal f1 f2 | _, _ -> false and eq_ml_pattern p1 p2 = match p1, p2 with @@ -430,7 +431,7 @@ let ast_iter_rel f = | MLapp (a,l) -> iter n a; List.iter (iter n) l | MLcons (_,_,l) | MLtuple l -> List.iter (iter n) l | MLmagic a -> iter n a - | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> () + | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ | MLfloat _ -> () in iter 0 (*s Map over asts. *) @@ -449,7 +450,8 @@ let ast_map f = function | MLcons (typ,c,l) -> MLcons (typ,c, List.map f l) | MLtuple l -> MLtuple (List.map f l) | MLmagic a -> MLmagic (f a) - | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ as a -> a + | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom + | MLuint _ | MLfloat _ as a -> a (*s Map over asts, with binding depth as parameter. *) @@ -467,7 +469,8 @@ let ast_map_lift f n = function | MLcons (typ,c,l) -> MLcons (typ,c, List.map (f n) l) | MLtuple l -> MLtuple (List.map (f n) l) | MLmagic a -> MLmagic (f n a) - | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ as a -> a + | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom + | MLuint _ | MLfloat _ as a -> a (*s Iter over asts. *) @@ -481,7 +484,8 @@ let ast_iter f = function | MLapp (a,l) -> f a; List.iter f l | MLcons (_,_,l) | MLtuple l -> List.iter f l | MLmagic a -> f a - | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> () + | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom + | MLuint _ | MLfloat _ -> () (*S Operations concerning De Bruijn indices. *) @@ -517,7 +521,7 @@ let nb_occur_match = | MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) l | MLcons (_,_,l) | MLtuple l -> List.fold_left (fun r a -> r+(nb k a)) 0 l | MLmagic a -> nb k a - | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> 0 + | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ | MLfloat _ -> 0 in nb 1 (* Replace unused variables by _ *) @@ -569,7 +573,7 @@ let dump_unused_vars a = let b' = ren env b in if b' == b then a else MLmagic b' - | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> a + | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ | MLfloat _ -> a and ren_branch env ((ids,p,b) as tr) = let occs = List.map (fun _ -> ref false) ids in @@ -1402,7 +1406,8 @@ let rec ml_size = function | MLfix(_,_,f) -> ml_size_array f | MLletin (_,_,t) -> ml_size t | MLmagic t -> ml_size t - | MLglob _ | MLrel _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> 0 + | MLglob _ | MLrel _ | MLexn _ | MLdummy _ | MLaxiom + | MLuint _ | MLfloat _ -> 0 and ml_size_list l = List.fold_left (fun a t -> a + ml_size t) 0 l -- cgit v1.2.3