diff --git a/doc/options.rst b/doc/options.rst index abedb7bbb..74b6493eb 100644 --- a/doc/options.rst +++ b/doc/options.rst @@ -82,14 +82,16 @@ export - ``xtc``: `XTC `__ format of the termination competition - ``raw_coq``: `Coq `__ format - ``stt_coq``: `Coq `__ format assuming that the input file is in an encoding of simple type theory + - ``raw_lean``: `Lean `__ format + - ``stt_lean``: `Lean `__ format assuming that the input file is in an encoding of simple type theory -**WARNING**: With the formats ``raw_coq``, ``stt_coq`` and ``raw_dk``, the translation is done just after parsing, thus before scoping and elaboration. So Lambdapi cannot translate any input file, and the output may be incomplete or fail to type-check. +**WARNING**: With the formats ``raw_coq``, ``stt_coq``, ``raw_lean``, ``stt_lean`` and ``raw_dk``, the translation is done just after parsing, thus before scoping and elaboration. So Lambdapi cannot translate any input file, and the output may be incomplete or fail to type-check. The format ``raw_dk`` does not accept the commands ``notation`` and ``inductive``, and proofs and tactics, which require elaboration. -The formats ``raw_coq`` and ``stt_coq`` only accept the commands ``require``, ``open``, ``symbol`` and ``rule``, but rules are simply ignored. The encoding of simple type theory can however be defined in Coq using `STTfa.v `__. +The formats ``raw_coq``, ``stt_coq``, ``raw_lean`` and ``stt_lean`` only accept the commands ``require``, ``open``, ``symbol`` and ``rule``, but rules are simply ignored. The encoding of simple type theory can however be defined in Coq using `STTfa.v `__. -For the format ``stt_coq``, several other options are available: +For the formats ``stt_coq`` and ``stt_lean``, several other options are available: * ``--encoding `` (mandatory option) where ```` contains the following sequence of builtin declarations: @@ -118,11 +120,11 @@ In symbol declarations or definitions, parameters with no type are assumed to be :: - builtin "coq_expr" ≔ lp_id; + builtin "expr" ≔ lp_id; -It instructs Lambdapi to replace any occurrence of the unqualified identifier ``lp_id`` by ``coq_expr``, which can be any Coq expression. Example: `renaming.lp `__. +It instructs Lambdapi to replace any occurrence of the unqualified identifier ``lp_id`` by ``expr``, which can be any expression. Example: `renaming.lp `__. -* ``--requiring `` to add ``Require Import `` at the beginning of the output. ``.v`` usually needs to contain at least the following definitions: +* ``--requiring `` to add ``Require Import `` at the beginning of the output. ``.v`` (and similarly ``.lean``) usually needs to contain at least the following definitions: :: diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml index 8bc4ffcaf..03f98f8ff 100644 --- a/src/cli/lambdapi.ml +++ b/src/cli/lambdapi.ml @@ -100,7 +100,8 @@ let parse_cmd : Config.t -> string list -> unit = fun cfg files -> Error.handle_exceptions run (** Possible outputs for the export command. *) -type output = Lp | Dk | RawDk | Hrs | Xtc | RawCoq | SttCoq +type output = + Lp | Dk | RawDk | Hrs | Xtc | RawCoq | SttCoq | RawLean | SttLean (** Running the export mode. *) let export_cmd (cfg:Config.t) (output:output option) (encoding:string option) @@ -109,8 +110,8 @@ let export_cmd (cfg:Config.t) (output:output option) (encoding:string option) (file:string) : unit = let run _ = Config.init {cfg with verbose = Some 0}; - Export.Coq.use_implicits := not no_implicits; - Export.Coq.use_notations := use_notations; + Export.Stt.use_implicits := not no_implicits; + Export.Stt.use_notations := use_notations; match output with | None | Some Lp -> Pretty.ast Format.std_formatter (Parser.parse_file file) @@ -121,16 +122,27 @@ let export_cmd (cfg:Config.t) (output:output option) (encoding:string option) | Some Xtc -> Export.Xtc.sign Format.std_formatter (Compile.compile_file file) | Some RawCoq -> - Export.Coq.stt := false; - Option.iter Export.Coq.set_renaming renaming; + Export.Stt.stt := false; + Option.iter Export.Stt.set_renaming renaming; Export.Coq.print (Parser.parse_file file) | Some SttCoq -> - Export.Coq.stt := true; - Option.iter Export.Coq.set_renaming renaming; - Option.iter Export.Coq.set_encoding encoding; - Option.iter Export.Coq.set_mapping mapping; - Option.iter Export.Coq.set_requiring requiring; + Export.Stt.stt := true; + Option.iter Export.Stt.set_renaming renaming; + Option.iter Export.Stt.set_encoding encoding; + Option.iter Export.Stt.set_mapping mapping; + Option.iter Export.Stt.set_requiring requiring; Export.Coq.print (Parser.parse_file file) + | Some RawLean -> + Export.Stt.stt := false; + Option.iter Export.Stt.set_renaming renaming; + Export.Lean.print file (Parser.parse_file file) + | Some SttLean -> + Export.Stt.stt := true; + Option.iter Export.Stt.set_renaming renaming; + Option.iter Export.Stt.set_encoding encoding; + Option.iter Export.Stt.set_mapping mapping; + Option.iter Export.Stt.set_requiring requiring; + Export.Lean.print file (Parser.parse_file file) in Error.handle_exceptions run (** Running the LSP server. *) @@ -235,6 +247,8 @@ let output : output option CLT.t = | "xtc" -> Ok Xtc | "raw_coq" -> Ok RawCoq | "stt_coq" -> Ok SttCoq + | "raw_lean" -> Ok RawLean + | "stt_lean" -> Ok SttLean | _ -> Error(`Msg "Invalid format") in let print fmt o = @@ -246,14 +260,16 @@ let output : output option CLT.t = | Hrs -> "hrs" | Xtc -> "xtc" | RawCoq -> "raw_coq" - | SttCoq -> "stt_coq") + | SttCoq -> "stt_coq" + | RawLean -> "raw_lean" + | SttLean -> "stt_lean") in Arg.conv (parse, print) in let doc = "Set the output format of the export command. The value of $(docv) \ - must be `lp' (default), `raw_dk`, `dk`, `hrs`, `xtc`, `raw_coq` or \ - `stt_coq`." + must be `lp' (default), `raw_dk`, `dk`, `hrs`, `xtc`, `raw_coq`, \ + `stt_coq`, `raw_lean` or `stt_lean`." in Arg.(value & opt (some output) None & info ["output";"o"] ~docv:"FMT" ~doc) @@ -263,7 +279,7 @@ let encoding : string option CLT.t = let print fmt s = string fmt s in Arg.conv (parse, print) in - let doc = "Set config file for the command export -o stt_coq." in + let doc = "Set config file for the command export -o stt_[coq|lean]." in Arg.(value & opt (some encoding) None & info ["encoding"] ~docv:"FILE" ~doc) let renaming : string option CLT.t = @@ -272,7 +288,7 @@ let renaming : string option CLT.t = let print fmt s = string fmt s in Arg.conv (parse, print) in - let doc = "Set config file for the command export -o stt_coq." in + let doc = "Set config file for the command export -o stt_[coq|lean]." in Arg.(value & opt (some renaming) None & info ["renaming"] ~docv:"FILE" ~doc) let mapping : string option CLT.t = @@ -281,7 +297,7 @@ let mapping : string option CLT.t = let print fmt s = string fmt s in Arg.conv (parse, print) in - let doc = "Set config file for the command export -o stt_coq." in + let doc = "Set config file for the command export -o stt_[coq|lean]." in Arg.(value & opt (some mapping) None & info ["mapping"] ~docv:"FILE" ~doc) let requiring : string option CLT.t = @@ -290,7 +306,7 @@ let requiring : string option CLT.t = let print fmt s = string fmt s in Arg.conv (parse, print) in - let doc = "Set config file for the command export -o stt_coq." in + let doc = "Set config file for the command export -o stt_[coq|lean]." in Arg.(value & opt (some requiring) None & info ["requiring"] ~docv:"FILE" ~doc) @@ -299,7 +315,7 @@ let no_implicits : bool CLT.t = Arg.(value & flag & info ["no-implicits"] ~doc) let use_notations : bool CLT.t = - let doc = "Generate Coq code using notations." in + let doc = "Generate code using notations." in Arg.(value & flag & info ["use-notations"] ~doc) (** Remaining arguments: source files. *) diff --git a/src/export/coq.ml b/src/export/coq.ml index 689330be4..c1bc6159a 100644 --- a/src/export/coq.ml +++ b/src/export/coq.ml @@ -18,190 +18,10 @@ The renaming map can be specified through a lambdapi file (option --renaming). open Lplib open Extra open Common open Pos open Error open Parsing open Syntax -open Core - -let log = Logger.make 'x' "xprt" "export" -let log = log.pp - -(** Symbols necessary to encode STT. *) - -type builtin = - Set | Prop | Arr | El | Imp | All | Prf | Eq | Or | And | Ex | Not - -let index_of_builtin = function - | Set -> 0 | Prop -> 1 | Arr -> 2 | El -> 3 | Imp -> 4 | All -> 5 - | Prf -> 6 | Eq -> 7 | Or -> 8 | And -> 9 | Ex -> 10 | Not -> 11 - -let nb_builtins = 12 - -let builtin_of_index = function - | 0 -> Set | 1 -> Prop | 2 -> Arr | 3 -> El | 4 -> Imp | 5 -> All - | 6 -> Prf | 7 -> Eq | 8 -> Or | 9 -> And | 10 -> Ex | 11 -> Not - | _ -> assert false - -let _ = (* sanity check *) - for i = 0 to nb_builtins - 1 do - assert (index_of_builtin (builtin_of_index i) = i) - done - -let index_of_name = function - | "Set" -> Some 0 | "prop" -> Some 1 | "arr" -> Some 2 | "El" -> Some 3 - | "imp" -> Some 4 | "all" -> Some 5 | "Prf" -> Some 6 | "eq" -> Some 7 - | "or" -> Some 8 | "and" -> Some 9 | "ex" -> Some 10 | "not" -> Some 11 - | _ -> None - -let name_of_index = function - | 0 -> "Set" | 1 -> "prop" | 2 -> "arr" | 3 -> "El" | 4 -> "imp"| 5 -> "all" - | 6 -> "Prf" | 7 -> "eq" | 8 -> "or" | 9 -> "and" | 10 -> "ex" | 11 -> "not" - | _ -> assert false - -let _ = (* sanity check *) - for i = 0 to nb_builtins - 1 do - assert (index_of_name (name_of_index i) = Some i) - done - -let builtin : Term.qident array = - let path = ["STTfa"] in - Array.init nb_builtins (fun i -> path, name_of_index i) - -let sym b = builtin.(index_of_builtin b) - -(** Set renaming map from file. *) - -let rmap = ref StrMap.empty - -let set_renaming : string -> unit = fun f -> - let consume = function - | {elt=P_builtin(coq_id,{elt=([],lp_id);_});_} -> - if Logger.log_enabled() then log "rename %s into %s" lp_id coq_id; - rmap := StrMap.add lp_id coq_id !rmap - | {pos;_} -> fatal pos "Invalid command." - in - Stream.iter consume (Parser.parse_file f) - -(** Set symbols whose declarations have to be erased. *) - -let erase = ref StrSet.empty - -module Qid = struct type t = Term.qident let compare = Stdlib.compare end -module QidMap = Map.Make(Qid) - -let map_erased_qid_coq = ref QidMap.empty - -let set_mapping : string -> unit = fun f -> - let consume = function - | {elt=P_builtin(coq_id,lp_qid);_} -> - if Logger.log_enabled() then - log "rename %a into %s" Pretty.qident lp_qid coq_id; - let id = snd lp_qid.elt in - if Logger.log_enabled() then log "erase %s" id; - erase := StrSet.add id !erase; - map_erased_qid_coq := - QidMap.add lp_qid.elt coq_id !map_erased_qid_coq; - if fst lp_qid.elt = [] && id <> coq_id then - rmap := StrMap.add id coq_id !rmap - | {pos;_} -> fatal pos "Invalid command." - in - Stream.iter consume (Parser.parse_file f) - -(** Set encoding. *) - -let map_qid_builtin = ref QidMap.empty - -let set_encoding : string -> unit = fun f -> - let found = Array.make nb_builtins false in - let consume = function - | {elt=P_builtin(n,lp_qid);pos} -> - begin match index_of_name n with - | Some i -> - if Logger.log_enabled() then - log "builtin \"%s\" = %a" n Pretty.qident lp_qid; - builtin.(i) <- lp_qid.elt; - found.(i) <- true; - let b = builtin_of_index i in - map_qid_builtin := QidMap.add lp_qid.elt b !map_qid_builtin; - if b = El || b = Prf then - (if Logger.log_enabled() then log "erase %s" (snd lp_qid.elt); - erase := StrSet.add (snd lp_qid.elt) !erase) - | None -> fatal pos "Unknown builtin." - end - | {pos;_} -> fatal pos "Invalid command." - in - Stream.iter consume (Parser.parse_file f); - Array.iteri - (fun i b -> - if not b then - let pos = - Some {fname=Some f;start_line=0;start_col=0;end_line=0;end_col=0} - in fatal pos "Builtin %s undefined." (name_of_index i)) - found - -(** Basic printing functions. We use Printf for efficiency reasons. *) -let out = Printf.printf - -let char = output_char -let string = output_string - -let prefix pre elt oc x = string oc pre; elt oc x -let suffix elt suf oc x = elt oc x; string oc suf - -let list elt sep oc xs = - match xs with - | [] -> () - | x::xs -> elt oc x; List.iter (prefix sep elt oc) xs - -(** Translation of identifiers. *) - -let translate_ident : string -> string = fun s -> - try StrMap.find s !rmap with Not_found -> s - -let raw_ident oc s = string oc (translate_ident s) - -let ident oc {elt;_} = raw_ident oc elt - -let param_id oc idopt = - match idopt with - | Some id -> ident oc id - | None -> char oc '_' - -let param_ids = list param_id " " - -let raw_path = list string "." - -let path oc {elt;_} = raw_path oc elt - -let qident oc {elt=(mp,s);_} = - match mp with - | [] -> raw_ident oc s - | _::_ -> raw_path oc mp; char oc '.'; raw_ident oc s +open Stt (** Translation of terms. *) -let stt = Stdlib.ref false -let use_implicits = Stdlib.ref false -let use_notations = Stdlib.ref false - -(* redefinition of p_get_args ignoring P_Wrap's. *) -let p_get_args : p_term -> p_term * p_term list = fun t -> - let rec p_get_args t acc = - match t.elt with - | P_Appl(t, u) -> p_get_args t (u::acc) - | P_Wrap t -> p_get_args t acc - | _ -> t, acc - in p_get_args t [] - -let app t default cases = - let h, ts = p_get_args t in - if !stt then - match h.elt with - | P_Iden({elt;_},expl) -> - begin match QidMap.find_opt elt !map_qid_builtin with - | None -> default h ts - | Some builtin -> cases h ts expl builtin - end - | _ -> default h ts - else default h ts - let rec term oc t = (*if Logger.log_enabled() then log "pp %a" (*Pos.short t.pos*) Pretty.term t;*) @@ -214,14 +34,14 @@ let rec term oc t = | P_Wild -> char oc '_' | P_NLit i -> if !stt then - match QidMap.find_opt ([],i) !map_erased_qid_coq with + match QidMap.find_opt ([],i) !map_erased_qid with | Some s -> string oc s | None -> raw_ident oc i else raw_ident oc i | P_Iden(qid,b) -> if b then char oc '@'; if !stt then - match QidMap.find_opt qid.elt !map_erased_qid_coq with + match QidMap.find_opt qid.elt !map_erased_qid with | Some s -> string oc s | None -> qident oc qid else qident oc qid @@ -292,8 +112,6 @@ and typopt oc t = Option.iter (prefix " : " term oc) t (** Translation of commands. *) -let is_lem x = is_opaq x || is_priv x - let command oc {elt; pos} = begin match elt with | P_open ps -> string oc "Import "; list path " " oc ps; string oc ".\n" @@ -344,18 +162,14 @@ let command oc {elt; pos} = | _ -> wrn pos "Command not translated." end -let ast oc = Stream.iter (command oc) +let commands oc = Stream.iter (command oc) (** Set Coq required file. *) -let require = ref None - -let set_requiring : string -> unit = fun f -> require := Some f - let print : ast -> unit = fun s -> let oc = stdout in begin match !require with | Some f -> string oc ("Require Import "^f^".\n") | None -> () end; - ast oc s + commands oc s diff --git a/src/export/lean.ml b/src/export/lean.ml new file mode 100644 index 000000000..4e80aff0d --- /dev/null +++ b/src/export/lean.ml @@ -0,0 +1,191 @@ +(** Translate the parser-level AST to Lean. + +There are two modes: + +- raw_lean mode (option -o raw_lean): translation of the AST as it is + (lambdapi-calculus is a subset system of lean if we ignore rules) + +- stt_lean mode (option -o stt_lean): translation of the AST as an encoding in + simple type theory. + + The encoding can be specified through a lambdapi file (option --encoding). + +In both modes, a renaming map can be provided to rename some identifiers. + +The renaming map can be specified through a lambdapi file (option --renaming). +*) + +open Lplib open Extra +open Common open Pos open Error +open Parsing open Syntax +open Stt + +(** Translation of terms. *) + +let rec term oc t = + (*if Logger.log_enabled() then + log "pp %a" (*Pos.short t.pos*) Pretty.term t;*) + match t.elt with + | P_Meta _ -> wrn t.pos "TODO"; assert false + | P_Patt _ -> wrn t.pos "TODO"; assert false + | P_Expl _ -> wrn t.pos "TODO"; assert false + | P_Type -> string oc "Type" + | P_Wild -> char oc '_' + | P_NLit i -> + if !stt then + match QidMap.find_opt ([],i) !map_erased_qid with + | Some s -> string oc s + | None -> raw_ident oc i + else raw_ident oc i + | P_Iden(qid,b) -> + if b then char oc '@'; + if !stt then + match QidMap.find_opt qid.elt !map_erased_qid with + | Some s -> string oc s + | None -> qident oc qid + else qident oc qid + | P_Arro(u,v) -> arrow oc u v + | P_Abst(xs,u) -> abst oc xs u + | P_Prod(xs,u) -> prod oc xs u + | P_LLet(x,xs,a,u,v) -> + string oc "let "; ident oc x; params_list oc xs; typopt oc a; + string oc " := "; term oc u; string oc " in "; term oc v + | P_Wrap u -> term oc u + | P_Appl _ -> + let default h ts = paren oc h; char oc ' '; list paren " " oc ts in + app t default + (fun h ts expl builtin -> + match !use_notations, !use_implicits && not expl, builtin, ts with + | _, _, (El|Prf), [u] -> term oc u + | _, _, (Arr|Imp), [u;v] -> arrow oc u v + | _, _, All, [_;{elt=P_Wrap({elt=P_Abst([_] as xs,u);_});_}] + | _, true, All, [{elt=P_Wrap({elt=P_Abst([_] as xs,u);_});_}] + -> prod oc xs u + | _, _, Ex, [_;{elt=P_Wrap({elt=P_Abst([x],u);_});_}] + | _, true, Ex, [{elt=P_Wrap({elt=P_Abst([x],u);_});_}] -> + string oc "exists "; raw_params oc x; string oc ", "; term oc u + | true, _, Eq, [_;u;v] + | true, true, Eq, [u;v] -> paren oc u; string oc " = "; paren oc v + | true, _, Or, [u;v] -> paren oc u; string oc " \\/ "; paren oc v + | true, _, And, [u;v] -> paren oc u; string oc " /\\ "; paren oc v + | true, _, Not, [u] -> string oc "~ "; paren oc u + | _ -> default h ts) + +and arrow oc u v = paren oc u; string oc " -> "; term oc v +and abst oc xs u = + string oc "fun"; params_list_in_abs oc xs; string oc " => "; term oc u +and prod oc xs u = + string oc "∀"; params_list_in_abs oc xs; string oc ", "; term oc u + +and paren oc t = + let default() = char oc '('; term oc t; char oc ')' in + match t.elt with + | P_Arro _ | P_Abst _ | P_Prod _ | P_LLet _ | P_Wrap _ -> default() + | P_Appl _ -> + app t (fun _ _ -> default()) + (fun _ ts _ builtin -> + match builtin, ts with + | (El|Prf), [u] -> paren oc u + | _ -> default()) + | _ -> term oc t + +and raw_params oc (ids,t,_) = param_ids oc ids; typopt oc t + +and params oc ((ids,t,b) as x) = + match b, t with + | true, _ -> char oc '{'; raw_params oc x; char oc '}' + | false, Some _ -> char oc '('; raw_params oc x; char oc ')' + | false, None -> param_ids oc ids + +(* starts with a space if the list is not empty *) +and params_list oc = List.iter (prefix " " params oc) + +(* starts with a space if the list is not empty *) +and params_list_in_abs oc l = + match l with + | [ids,t,false] -> char oc ' '; param_ids oc ids; typopt oc t + | _ -> params_list oc l + +(* starts with a space if <> None *) +and typopt oc t = Option.iter (prefix " : " term oc) t + +(** Translation of commands. *) + +let req_mod oc p = string oc "import "; path oc p; string oc "\n" +let open_mod oc p = string oc "open "; path oc p; string oc "\n" + +let openings = ref [] + +let command oc {elt; pos} = + begin match elt with + | P_open ps -> List.iter (open_mod oc) ps + | P_require (b, ps) -> + List.iter (req_mod oc) ps; + if b then openings := List.rev_append ps !openings + | P_require_as _ -> wrn pos "Command not translated." + | P_symbol + { p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ; + p_sym_trm; p_sym_prf=_; p_sym_def } -> + if not (StrSet.mem p_sym_nam.elt !erase) then + let p_sym_arg = + if !stt then + let pos = None in + (* Parameters with no type are assumed to be of type [Set]. *) + let _Set = {elt=P_Iden({elt=sym Set;pos},false);pos} in + List.map (function ids, None, b -> ids, Some _Set, b | x -> x) + p_sym_arg + else p_sym_arg + in + begin match p_sym_def, p_sym_trm, p_sym_arg, p_sym_typ with + | true, Some t, _, Some a when List.exists is_lem p_sym_mod -> + (* If they have a type, opaque or private defined symbols are + translated as Lemma's so that their definition is loaded in + memory only when it is necessary. *) + string oc "theorem "; ident oc p_sym_nam; + params_list oc p_sym_arg; string oc " : "; term oc a; + string oc " := "; term oc t; string oc "\n" + | true, Some t, _, _ -> + if List.exists is_opaq p_sym_mod then string oc "opaque " + else string oc "noncomputable def "; + ident oc p_sym_nam; + params_list oc p_sym_arg; typopt oc p_sym_typ; + string oc " := "; term oc t; string oc "\n" + | false, _, [], Some t -> + string oc "axiom "; ident oc p_sym_nam; string oc " : "; + term oc t; string oc "\n" + | false, _, _, Some t -> + string oc "axiom "; ident oc p_sym_nam; + string oc " : ∀"; params_list oc p_sym_arg; string oc ", "; + term oc t; string oc "\n" + | _ -> wrn pos "Command not translated." + end + | _ -> wrn pos "Command not translated." + end + +let commands oc = Stream.iter (command oc) + +let handle_requires s = + let rec handle_next_elt() = + let x = Stream.next s in + match x.elt with + | P_require (b, ps) -> + List.iter (req_mod stdout) ps; + if b then openings := List.rev_append ps !openings; + handle_next_elt() + | _ -> Some x + in + try handle_next_elt() with Stream.Failure -> None + +let print : string -> ast -> unit = fun file s -> + let oc = stdout in + Option.iter (fun s -> string oc ("import "^s^"\n")) !require; + match handle_requires s with + | None -> () + | Some c -> + Option.iter (fun s -> string oc ("open "^s^"\n")) !require; + List.iter (open_mod oc) (List.rev !openings); + string oc "\nnamespace "; + string oc (Filename.chop_extension file); + string oc "\n\n"; + command oc c; + commands oc s diff --git a/src/export/stt.ml b/src/export/stt.ml new file mode 100644 index 000000000..7eba1e849 --- /dev/null +++ b/src/export/stt.ml @@ -0,0 +1,197 @@ +(** Base module for translating lp proofs encoded in simple type theory. *) + +open Lplib open Extra +open Common open Pos open Error +open Parsing open Syntax +open Core + +let log = Logger.make 'x' "xprt" "export" +let log = log.pp + +(** Symbols necessary to encode STT. *) + +type builtin = + Set | Prop | Arr | El | Imp | All | Prf | Eq | Or | And | Ex | Not + +let index_of_builtin = function + | Set -> 0 | Prop -> 1 | Arr -> 2 | El -> 3 | Imp -> 4 | All -> 5 + | Prf -> 6 | Eq -> 7 | Or -> 8 | And -> 9 | Ex -> 10 | Not -> 11 + +let nb_builtins = 12 + +let builtin_of_index = function + | 0 -> Set | 1 -> Prop | 2 -> Arr | 3 -> El | 4 -> Imp | 5 -> All + | 6 -> Prf | 7 -> Eq | 8 -> Or | 9 -> And | 10 -> Ex | 11 -> Not + | _ -> assert false + +let _ = (* sanity check *) + for i = 0 to nb_builtins - 1 do + assert (index_of_builtin (builtin_of_index i) = i) + done + +let index_of_name = function + | "Set" -> Some 0 | "prop" -> Some 1 | "arr" -> Some 2 | "El" -> Some 3 + | "imp" -> Some 4 | "all" -> Some 5 | "Prf" -> Some 6 | "eq" -> Some 7 + | "or" -> Some 8 | "and" -> Some 9 | "ex" -> Some 10 | "not" -> Some 11 + | _ -> None + +let name_of_index = function + | 0 -> "Set" | 1 -> "prop" | 2 -> "arr" | 3 -> "El" | 4 -> "imp"| 5 -> "all" + | 6 -> "Prf" | 7 -> "eq" | 8 -> "or" | 9 -> "and" | 10 -> "ex" | 11 -> "not" + | _ -> assert false + +let _ = (* sanity check *) + for i = 0 to nb_builtins - 1 do + assert (index_of_name (name_of_index i) = Some i) + done + +let builtin : Term.qident array = + let path = ["STTfa"] in + Array.init nb_builtins (fun i -> path, name_of_index i) + +let sym b = builtin.(index_of_builtin b) + +(** Set renaming map from file. *) + +let rmap = ref StrMap.empty + +let set_renaming : string -> unit = fun f -> + let consume = function + | {elt=P_builtin(lean_id,{elt=([],lp_id);_});_} -> + if Logger.log_enabled() then log "rename %s into %s" lp_id lean_id; + rmap := StrMap.add lp_id lean_id !rmap + | {pos;_} -> fatal pos "Invalid command." + in + Stream.iter consume (Parser.parse_file f) + +(** Set symbols whose declarations have to be erased. *) + +let erase = ref StrSet.empty + +module Qid = struct type t = Term.qident let compare = Stdlib.compare end +module QidMap = Map.Make(Qid) + +let map_erased_qid = ref QidMap.empty + +let set_mapping : string -> unit = fun f -> + let consume = function + | {elt=P_builtin(lean_id,lp_qid);_} -> + if Logger.log_enabled() then + log "rename %a into %s" Pretty.qident lp_qid lean_id; + let id = snd lp_qid.elt in + if Logger.log_enabled() then log "erase %s" id; + erase := StrSet.add id !erase; + map_erased_qid := + QidMap.add lp_qid.elt lean_id !map_erased_qid; + if fst lp_qid.elt = [] && id <> lean_id then + rmap := StrMap.add id lean_id !rmap + | {pos;_} -> fatal pos "Invalid command." + in + Stream.iter consume (Parser.parse_file f) + +(** Set encoding. *) + +let map_qid_builtin = ref QidMap.empty + +let set_encoding : string -> unit = fun f -> + let found = Array.make nb_builtins false in + let consume = function + | {elt=P_builtin(n,lp_qid);pos} -> + begin match index_of_name n with + | Some i -> + if Logger.log_enabled() then + log "builtin \"%s\" = %a" n Pretty.qident lp_qid; + builtin.(i) <- lp_qid.elt; + found.(i) <- true; + let b = builtin_of_index i in + map_qid_builtin := QidMap.add lp_qid.elt b !map_qid_builtin; + if b = El || b = Prf then + (if Logger.log_enabled() then log "erase %s" (snd lp_qid.elt); + erase := StrSet.add (snd lp_qid.elt) !erase) + | None -> fatal pos "Unknown builtin." + end + | {pos;_} -> fatal pos "Invalid command." + in + Stream.iter consume (Parser.parse_file f); + Array.iteri + (fun i b -> + if not b then + let pos = + Some {fname=Some f;start_line=0;start_col=0;end_line=0;end_col=0} + in fatal pos "Builtin %s undefined." (name_of_index i)) + found + +(** Basic printing functions. We use Printf for efficiency reasons. *) + +let out = Printf.printf + +let char = output_char +let string = output_string + +let prefix pre elt oc x = string oc pre; elt oc x +let suffix elt suf oc x = elt oc x; string oc suf + +let list elt sep oc xs = + match xs with + | [] -> () + | x::xs -> elt oc x; List.iter (prefix sep elt oc) xs + +(** Translation of identifiers. *) + +let translate_ident : string -> string = fun s -> + try StrMap.find s !rmap with Not_found -> s + +let raw_ident oc s = string oc (translate_ident s) + +let ident oc {elt;_} = raw_ident oc elt + +let param_id oc idopt = + match idopt with + | Some id -> ident oc id + | None -> char oc '_' + +let param_ids = list param_id " " + +let raw_path = list string "." + +let path oc {elt;_} = raw_path oc elt + +let qident oc {elt=(mp,s);_} = + match mp with + | [] -> raw_ident oc s + | _::_ -> raw_path oc mp; char oc '.'; raw_ident oc s + +(** Translation of terms. *) + +let stt = Stdlib.ref false +let use_implicits = Stdlib.ref false +let use_notations = Stdlib.ref false + +(* redefinition of p_get_args ignoring P_Wrap's. *) +let p_get_args : p_term -> p_term * p_term list = fun t -> + let rec p_get_args t acc = + match t.elt with + | P_Appl(t, u) -> p_get_args t (u::acc) + | P_Wrap t -> p_get_args t acc + | _ -> t, acc + in p_get_args t [] + +let app t default cases = + let h, ts = p_get_args t in + if !stt then + match h.elt with + | P_Iden({elt;_},expl) -> + begin match QidMap.find_opt elt !map_qid_builtin with + | None -> default h ts + | Some builtin -> cases h ts expl builtin + end + | _ -> default h ts + else default h ts + +let is_lem x = is_opaq x || is_priv x + +(** Set required file. *) + +let require = ref None + +let set_requiring : string -> unit = fun f -> require := Some f diff --git a/tests/regressions/dune b/tests/regressions/dune index 1c0302f40..0f934135b 100644 --- a/tests/regressions/dune +++ b/tests/regressions/dune @@ -1,5 +1,5 @@ (tests (names hrs xtc dtrees) (libraries timed lambdapi.export lambdapi.core lambdapi.common lambdapi.handle) - (deps ../OK/boolean.lp ../OK/unif_hint.lp ../lambdapi.pkg) + (deps ../OK/group.lp ../OK/boolean.lp ../OK/unif_hint.lp ../lambdapi.pkg) )