From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- plugins/extraction/haskell.ml | 47 ++++++++++++++++++++++--------------------- 1 file changed, 24 insertions(+), 23 deletions(-) (limited to 'plugins/extraction/haskell.ml') diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 0692c88c..e6234c14 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Id.Set.add (Id.of_string s)) @@ -58,7 +60,6 @@ let preamble mod_name comment used_modules usf = else str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++ str "import qualified GHC.Base" ++ fnl () ++ - str "import qualified GHC.Prim" ++ fnl () ++ str "#else" ++ fnl () ++ str "-- HUGS" ++ fnl () ++ str "import qualified IOExts" ++ fnl () ++ @@ -78,7 +79,7 @@ let preamble mod_name comment used_modules usf = (if not usf.tunknown then mt () else str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++ - str "type Any = GHC.Prim.Any" ++ fnl () ++ + str "type Any = GHC.Base.Any" ++ fnl () ++ str "#else" ++ fnl () ++ str "-- HUGS" ++ fnl () ++ str "type Any = ()" ++ fnl () ++ @@ -92,7 +93,7 @@ let preamble mod_name comment used_modules usf = let pp_abst = function | [] -> (mt ()) | l -> (str "\\" ++ - prlist_with_sep (fun () -> (str " ")) pr_id l ++ + prlist_with_sep (fun () -> (str " ")) Id.print l ++ str " ->" ++ spc ()) (*s The pretty-printer for haskell syntax *) @@ -108,7 +109,7 @@ let rec pp_type par vl t = let rec pp_rec par = function | Tmeta _ | Tvar' _ -> assert false | Tvar i -> - (try pr_id (List.nth vl (pred i)) + (try Id.print (List.nth vl (pred i)) with Failure _ -> (str "a" ++ int i)) | Tglob (r,[]) -> pp_global Type r | Tglob (IndRef(kn,0),l) @@ -145,9 +146,9 @@ let rec pp_expr par env args = | MLrel n -> let id = get_db_name n env in (* Try to survive to the occurrence of a Dummy rel. - TODO: we should get rid of this hack (cf. #592) *) + TODO: we should get rid of this hack (cf. BZ#592) *) let id = if Id.equal id dummy_name then Id.of_string "__" else id in - apply (pr_id id) + apply (Id.print id) | MLapp (f,args') -> let stl = List.map (pp_expr true env []) args' in pp_expr par env (stl @ args) f @@ -158,7 +159,7 @@ let rec pp_expr par env args = apply2 st | MLletin (id,a1,a2) -> let i,env' = push_vars [id_of_mlid id] env in - let pp_id = pr_id (List.hd i) + let pp_id = Id.print (List.hd i) and pp_a1 = pp_expr false env [] a1 and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in let pp_def = @@ -185,7 +186,7 @@ let rec pp_expr par env args = pp_boxed_tuple (pp_expr true env []) l | MLcase (_,t, pv) when is_custom_match pv -> if not (is_regular_match pv) then - error "Cannot mix yet user-given match and general patterns."; + user_err Pp.(str "Cannot mix yet user-given match and general patterns."); let mkfun (ids,_,e) = if not (List.is_empty ids) then named_lams (List.rev ids) e else dummy_lams (ast_lift 1 e) 1 @@ -222,10 +223,10 @@ and pp_cons_pat par r ppl = and pp_gen_pat par ids env = function | Pcons (r,l) -> pp_cons_pat par r (List.map (pp_gen_pat true ids env) l) - | Pusual r -> pp_cons_pat par r (List.map pr_id ids) + | Pusual r -> pp_cons_pat par r (List.map Id.print ids) | Ptuple l -> pp_boxed_tuple (pp_gen_pat false ids env) l | Pwild -> str "_" - | Prel n -> pr_id (get_db_name n env) + | Prel n -> Id.print (get_db_name n env) and pp_one_pat env (ids,p,t) = let ids',env' = push_vars (List.rev_map id_of_mlid ids) env in @@ -250,10 +251,10 @@ and pp_fix par env i (ids,bl) args = (v 0 (v 1 (str "let {" ++ fnl () ++ prvect_with_sep (fun () -> str ";" ++ fnl ()) - (fun (fi,ti) -> pp_function env (pr_id fi) ti) + (fun (fi,ti) -> pp_function env (Id.print fi) ti) (Array.map2 (fun a b -> a,b) ids bl) ++ str "}") ++ - fnl () ++ str "in " ++ pp_apply (pr_id ids.(i)) false args)) + fnl () ++ str "in " ++ pp_apply (Id.print ids.(i)) false args)) and pp_function env f t = let bl,t' = collect_lams t in @@ -265,19 +266,19 @@ and pp_function env f t = (*s Pretty-printing of inductive types declaration. *) let pp_logical_ind packet = - pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++ + pp_comment (Id.print packet.ip_typename ++ str " : logical inductive") ++ pp_comment (str "with constructors : " ++ - prvect_with_sep spc pr_id packet.ip_consnames) + prvect_with_sep spc Id.print packet.ip_consnames) let pp_singleton kn packet = let name = pp_global Type (IndRef (kn,0)) in let l = rename_tvars keywords packet.ip_vars in hov 2 (str "type " ++ name ++ spc () ++ - prlist_with_sep spc pr_id l ++ + prlist_with_sep spc Id.print l ++ (if not (List.is_empty l) then str " " else mt ()) ++ str "=" ++ spc () ++ pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++ pp_comment (str "singleton inductive, whose constructor was " ++ - pr_id packet.ip_consnames.(0))) + Id.print packet.ip_consnames.(0))) let pp_one_ind ip pl cv = let pl = rename_tvars keywords pl in @@ -329,7 +330,7 @@ let pp_decl = function let ids,s = find_type_custom r in prlist (fun id -> str (id^" ")) ids ++ str "=" ++ spc () ++ str s with Not_found -> - prlist (fun id -> pr_id id ++ str " ") l ++ + prlist (fun id -> Id.print id ++ str " ") l ++ if t == Taxiom then str "= () -- AXIOM TO BE REALIZED" ++ fnl () else str "=" ++ spc () ++ pp_type false l t in -- cgit v1.2.3