From 12b7a93d15034b2eb35f3244cd998e04bb714e15 Mon Sep 17 00:00:00 2001 From: Peter Sewell Date: Sat, 14 Feb 2026 21:38:46 +0000 Subject: [PATCH 1/5] WIP hackish minimal support for Lean generation --- examples/1Bsemantics/Makefile | 6 +- examples/1Bsemantics/l1.ott | 2 +- src/auxl.ml | 11 ++- src/context_pp.ml | 8 +- src/defns.ml | 70 ++++++++++++-- src/embed_pp.ml | 5 +- src/grammar_pp.ml | 171 ++++++++++++++++++++++++++-------- src/grammar_typecheck.ml | 25 ++--- src/main.ml | 20 +++- src/subrules_pp.ml | 20 +++- src/substs_pp.ml | 126 ++++++++++++++++++++++--- src/system_pp.ml | 15 +++ src/types.ml | 9 ++ 13 files changed, 401 insertions(+), 87 deletions(-) diff --git a/examples/1Bsemantics/Makefile b/examples/1Bsemantics/Makefile index 380572b..c891be2 100644 --- a/examples/1Bsemantics/Makefile +++ b/examples/1Bsemantics/Makefile @@ -1,9 +1,9 @@ -#OTT=../../bin/ott -OTT=ott +OTT=../../bin/ott +#OTT=ott l1: l1.ott - $(OTT) -pp_grammar -isa_syntax true l1.ott -o l1.tex -o l1.thy -o l1.lem -o l1.v + $(OTT) -pp_grammar -isa_syntax true l1.ott -o l1.tex -o l1.v -o l1.lean # -o l1.thy -o l1.lem $(OTT) -tex_wrap false l1.ott -o l1_nowrap.tex pdflatex l1.tex lem l1.lem -isa diff --git a/examples/1Bsemantics/l1.ott b/examples/1Bsemantics/l1.ott index 40f00b5..c41f609 100644 --- a/examples/1Bsemantics/l1.ott +++ b/examples/1Bsemantics/l1.ott @@ -30,7 +30,7 @@ e :: 'E_' ::= {{ com expressions }} | skip :: :: skip | e1 ; e2 :: :: sequence | while e1 do e2 :: :: while - | ( e ) :: M :: paren {{ ichlo ([[e]]) }} + | ( e ) :: M :: paren {{ ichlo ([[e]]) }} {{ lean ([[e]]) }} v :: 'V_' ::= {{ com values }} | n :: :: num diff --git a/src/auxl.ml b/src/auxl.ml index 88ee363..2276dc7 100644 --- a/src/auxl.ml +++ b/src/auxl.ml @@ -48,6 +48,7 @@ let mode_name m = match m with | Hol _ -> "HOL" | Lem _ -> "Lem" | Coq _ -> "Coq" + | Lean _ -> "Lean" | Twf _ -> "Twelf" | Caml _ -> "OCaml" | Lex _ -> "Lex" @@ -602,6 +603,7 @@ let hom_name_for_pp_mode m | Isa _ -> "isa" | Hol _ -> "hol" | Lem _ -> "lem" + | Lean _ -> "lean" | Coq _ -> "coq" | Twf _ -> "twf" | Caml _ -> "ocaml" @@ -818,6 +820,7 @@ let split3 (l : ('a * 'b * 'c) list) : 'a list * 'b list * 'c list = let big_line_comment m s = match m with | Coq _ | Hol _ | Lem _ | Isa _ | Caml _ -> "(** "^s^" *)\n" + | Lean _ -> "/- - "^s^" - -/\n" | Twf _ -> "%%% "^s^" %%%\n\n" | Tex _ -> "% "^s^"\n" | Menhir _ | Lex _ | Ascii _ -> errorm m "big_line_comment" @@ -1604,7 +1607,7 @@ let pp_true m in_prop = else "true" | Hol _ -> "T" | Caml _ -> "true" - | Lem _ -> "true" + | Lem _ | Lean _ -> "true" | Ascii _ | Tex _ | Twf _ | Lex _ | Menhir _ -> errorm m "pp_true" let pp_false m in_prop = @@ -1616,7 +1619,7 @@ let pp_false m in_prop = else "false" | Hol _ -> "F" | Caml _ -> "false" - | Lem _ -> "false" + | Lem _ | Lean _ -> "false" | Ascii _ | Tex _ | Twf _ | Lex _ | Menhir _ -> errorm m "pp_false" let pp_and m in_prop = @@ -1629,6 +1632,7 @@ let pp_and m in_prop = then " /\\ " else " && " | Hol _ -> " /\\ " + | Lean _ -> " /\\ " | Ascii _ | Tex _ | Twf _ | Lex _ | Menhir _ -> errorm m "pp_and" let pp_or m in_prop = @@ -1639,6 +1643,7 @@ let pp_or m in_prop = then " \\/ " else " || " | Hol _ -> " \\/ " + | Lean _ -> " \\/ " | Caml _ -> " || " | Lem _ -> " || " | Ascii _ | Tex _ | Twf _ | Lex _ | Menhir _ -> errorm m "pp_or" @@ -1684,7 +1689,7 @@ let insert_append m l = ^ ( String.concat " <- " (List.map2 (fun s nl -> s ^ " " ^ nl) l list_nl) ) ^ final_append ) - | Caml _ | Tex _ | Ascii _ | Hol _ | Lem _ | Isa _ | Lex _ | Menhir _ -> raise ThisCannotHappen + | Caml _ | Tex _ | Ascii _ | Hol _ | Lem _ | Lean _ | Isa _ | Lex _ | Menhir _ -> raise ThisCannotHappen (* skip a nonterm or a metavar in a list of elements *) let rec skip_nt_mv (es:element list) = diff --git a/src/context_pp.ml b/src/context_pp.ml index 0bcf113..3d87ad3 100644 --- a/src/context_pp.ml +++ b/src/context_pp.ml @@ -101,7 +101,7 @@ let pp_prod_context m xd lookup (hole:nonterm) (target:nontermroot) (r:rule) (p: let lhs_pat = Grammar_pp.pp_symterm m xd sie de lhs_st in let lhs = ( match m with - | Coq _ | Caml _ -> lhs_pat + | Coq _ | Lean _ | Caml _ -> lhs_pat | Isa _ | Hol _ | Lem _ | Twf _ -> lhs_pat ^ " " ^ Grammar_pp.pp_nonterm m xd hole | Lex _ | Menhir _ | Tex _ | Ascii _ -> assert false) in (* compute the rhs *) @@ -130,6 +130,12 @@ let pp_rule_context m xd lookup cr : int_func = ^ ") ("^fake_hole_var^":"^ Grammar_pp.pp_nontermroot_ty m xd cr.cr_hole ^")", "", " : " ^ (Grammar_pp.pp_nontermroot_ty m xd cr.cr_target) ^ " :=\n match "^ctx_var^" with\n") + | Lean _ -> + ((leanTODO "6" ( id + ^ " ("^ctx_var^":"^ Grammar_pp.pp_nontermroot_ty m xd cr.cr_ntr + ^ ") ("^fake_hole_var^":"^ Grammar_pp.pp_nontermroot_ty m xd cr.cr_hole ^")")), + "", + " : " ^ (Grammar_pp.pp_nontermroot_ty m xd cr.cr_target) ^ " :=\n match "^ctx_var^" with\n") | Isa _ -> ( id ^ " :: \"" ^ Grammar_pp.pp_nontermroot_ty m xd cr.cr_ntr ^ " => " diff --git a/src/defns.ml b/src/defns.ml index 90727f6..e3f9dac 100644 --- a/src/defns.ml +++ b/src/defns.ml @@ -79,7 +79,7 @@ let pp_subntr (m: pp_mode) (xd: syntaxdefn): (nontermroot * nontermroot * nonter Auxl.pp_is ntrl ntru ^ " " ^ Auxl.hide_isa_trailing_underscore m (( match m with Twf _ -> String.uppercase_ascii ntr' - | Coq _ | Isa _ | Hol _ | Lem _ -> ntr' + | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ -> ntr' | Caml _ | Tex _ | Ascii _ | Lex _ | Menhir _ -> raise Auxl.ThisCannotHappen ) ^ Grammar_pp.pp_suffix_with_sie m xd Bounds.sie_project suff) in ( match m with @@ -117,6 +117,11 @@ let pp_listsubntr : pp_mode -> syntaxdefn -> ((nontermroot * nontermroot * nonte ^ "(fun "^pp_pattern^" -> "^pp_subntr m xd subntr^") " ^ pp_squished_vars + | Lean _ -> + leanTODO "17" "List.all " + ^ "(fun "^pp_pattern^" -> "^pp_subntr m xd subntr^") " + ^ pp_squished_vars + | Coq co -> let ty_list = Str.split (Str.regexp "(\\|*\\|)") coq_type_pattern in if String.contains coq_type_pattern '*' @@ -245,7 +250,7 @@ let pp_drule fd (m:pp_mode) (xd:syntaxdefn) (dr:drule) : unit = (Grammar_pp.pp_tex_DRULE_NAME_NAME m) (Auxl.pp_tex_escape dr.drule_name) pp_com - | Isa _ | Hol _ | Lem _ | Coq _ | Twf _ -> + | Isa _ | Hol _ | Lem _ | Coq _ | Lean _ | Twf _ -> let non_free_ntrs = Subrules_pp.non_free_ntrs m xd xd.xd_srs in (* find all the nonterms used at non-free types *) @@ -277,7 +282,7 @@ let pp_drule fd (m:pp_mode) (xd:syntaxdefn) (dr:drule) : unit = List.map (pp_subntr m xd) nonlist_subntrs @ pp_listsubntr m xd list_subntrs in - (* collect all the isa/coq/hol variables that should be quantified *) + (* collect all the isa/coq/hol/lean variables that should be quantified *) (* for this clause *) let quantified_proof_assistant_vars = @@ -402,6 +407,43 @@ let pp_drule fd (m:pp_mode) (xd:syntaxdefn) (dr:drule) : unit = output_string fd ppd_conclusion; output_string fd "\n\n" + + | Lean _ -> + Printf.fprintf fd "%s%s%s: " + (leanTODO "18" "") + "" (*("(*"^Location.pp_loc dr.drule_loc^"*)")*) + dr.drule_name; +(* Lem currrently requires a forall even if there are no quantified variables, + and a "true ==>" if there are no premises *) +(* + (match quantified_proof_assistant_vars with + | [] -> () + | _ -> +*) + output_string fd "forall"; + List.iter (fun (var,ty,_) -> Printf.fprintf fd " %s" (leanTODO "19" var)) + quantified_proof_assistant_vars; +(* List.iter (fun (var,ty,_) -> Printf.fprintf fd " (%s:%s)" var ty) + quantified_proof_assistant_vars;*) + output_string fd " .\n"; +(* +); +*) + if (snd ppd_premises)<>[] || ppd_subntrs<>[] then + begin + (* output_string fd " &&\n(";*) + iter_asep fd " /\\n" + (fun s -> output_string fd "("; output_string fd s; output_string fd ")") + (ppd_subntrs @ snd ppd_premises); + output_string fd "\n" + end + else + output_string fd "true\n"; + output_string fd " ==> \n"; + output_string fd ppd_conclusion; + output_string fd "\n\n" + + | Coq co -> let rec remove_dupl l = match l with | [] -> [] @@ -484,6 +526,9 @@ let pp_defn fd (m:pp_mode) (xd:syntaxdefn) lookup (defnclass_wrapper:string) (un | Lem _ -> Printf.fprintf fd "(* defn %s *)\n\n" d.d_name; iter_sep (pp_processed_semiraw_rule fd m xd) "and\n" d.d_rules + | Lean _ -> + Printf.fprintf fd "/- defn %s -/\n\n" d.d_name; + iter_sep (pp_processed_semiraw_rule fd m xd) (leanTODO "20" "and\n") d.d_rules | Coq co -> (* FZ factor this code ? *) let prod_name = defnclass_wrapper ^ d.d_name in @@ -626,6 +671,12 @@ let pp_defnclass fd (m:pp_mode) (xd:syntaxdefn) lookup (dc:defnclass) = List.iter (output_string fd) !(co.coq_list_aux_defns.newly_defined); output_string fd ".\n" + | Lean co -> + Printf.fprintf fd "\n/- defns %s -/\ninductive " dc.dc_name; + iter_asep fd "\nwhere " + (fun d -> pp_defn fd m xd lookup dc.dc_wrapper universe d) + dc.dc_defns + | Twf wo -> let twf_type_of_defn : syntaxdefn -> defn -> string = fun xd d -> @@ -669,7 +720,7 @@ let pp_funclause (m:pp_mode) (xd:syntaxdefn) (fc:funclause) : string = ppd_lhs ^ " === " ^ ppd_rhs ^ "\n" | Tex _ -> Grammar_pp.pp_tex_FUNCLAUSE_NAME m^"{"^ppd_lhs^"}"^"{"^ppd_rhs^"}%\n" - | Isa _ | Hol _ | Lem _ | Coq _ | Caml _ | Twf _ | Lex _ | Menhir _ -> + | Isa _ | Hol _ | Lem _ | Coq _ | Lean _ | Caml _ | Twf _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_funclause" let rec insert_commas l = @@ -694,7 +745,7 @@ let pp_symterm_node_lhs m xd sie de st = with Not_found -> Auxl.int_error "pp_symterm_node_lhs" in let hom = match m with - | Coq _ | Caml _ | Lem _ (* LemTODO4: really? *) -> (insert_commas hom) + | Coq _ | Lean _ | Caml _ | Lem _ (* LemTODO4: really? *) -> (insert_commas hom) | Hol _ | Isa _ -> hom | Twf _ | Ascii _ | Tex _ | Lex _ | Menhir _ -> raise Auxl.ThisCannotHappen in String.concat " " (Grammar_pp.apply_hom_spec m xd hom pes) @@ -850,7 +901,7 @@ let pp_fundefn (m:pp_mode) (xd:syntaxdefn) lookup (fd:fundefn) : string = ^ "\\end{"^Grammar_pp.pp_tex_FUNDEFN_BLOCK_NAME m ^"}" ^ "}\n\n" - | Isa _ | Hol _ | Lem _ | Coq _ | Twf _ | Caml _ | Lex _ | Menhir _ -> + | Isa _ | Hol _ | Lem _ | Coq _ | Lean _ | Twf _ | Caml _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_fundefn" let pp_fundefnclass (m:pp_mode) (xd:syntaxdefn) lookup (fdc:fundefnclass) : string = @@ -873,7 +924,7 @@ let pp_fundefnclass (m:pp_mode) (xd:syntaxdefn) lookup (fdc:fundefnclass) : stri (List.map (function fd -> Grammar_pp.tex_fundefn_name m fd.fd_name^"{}") fdc.fdc_fundefns)) ^ "}\n\n" - | Isa _ | Coq _ | Hol _ | Lem _ | Caml _ -> + | Isa _ | Coq _ | Lean _ | Hol _ | Lem _ | Caml _ -> let proof = let pp_proof h = ( match h with @@ -881,7 +932,7 @@ let pp_fundefnclass (m:pp_mode) (xd:syntaxdefn) lookup (fdc:fundefnclass) : stri | None -> None | _ -> Auxl.warning (Some fdc.fdc_loc) "malformed isa-proof/hol-proof hom"; Some "<<>>" ) in ( match m with - | Coq _ | Caml _ | Lem _ -> None + | Coq _ | Caml _ | Lem _ | Lean _ -> None | Isa _ -> pp_proof (Auxl.hom_spec_for_hom_name "isa-proof" fdc.fdc_homs) | Hol _ -> pp_proof (Auxl.hom_spec_for_hom_name "hol-proof" fdc.fdc_homs) | _ -> raise Auxl.ThisCannotHappen ) in @@ -951,6 +1002,9 @@ let pp_fun_or_reln_defnclass_list | Twf _ -> output_string fd "%%% definitions %%%\n\n"; List.iter (fun frdc -> pp_fun_or_reln_defnclass fd m xd lookup frdc) frdcs + | Lean _ -> + output_string fd "/- definitions -/\n\n"; + List.iter (fun frdc -> pp_fun_or_reln_defnclass fd m xd lookup frdc) frdcs | Coq co -> pp_auxiliary_list_rules fd m xd frdcs; output_string fd "(* definitions *)\n"; diff --git a/src/embed_pp.ml b/src/embed_pp.ml index 1ab5ef9..f0d46a4 100644 --- a/src/embed_pp.ml +++ b/src/embed_pp.ml @@ -56,6 +56,7 @@ and pp_embedmorphism fd m xd lookup (l,hn,es) = output_string fd Grammar_pp.pp_DOUBLERIGHTBRACE; output_string fd "\n"; | (Coq _, "coq") + | (Lean _, "lean") | (Isa _, "isa") | (Hol _, "hol") | (Lem _, "lem") @@ -72,7 +73,7 @@ and pp_embedmorphism fd m xd lookup (l,hn,es) = | (Isa io, "isa-lib") -> let x = io.isa_library in x := (fst !x, embed_strings (snd !x) es) - | (Coq _, _) | (Isa _, _) | (Hol _,_) | (Lem _,_) | (Twf _,_) | (Tex _,_) | (Caml _,_) | (Lex _, _) | (Menhir _, _) -> () + | (Coq _, _) | (Lean _, _) | (Isa _, _) | (Hol _,_) | (Lem _,_) | (Twf _,_) | (Tex _,_) | (Caml _,_) | (Lex _, _) | (Menhir _, _) -> () and pp_embed_spec fd m xd lookup es = List.iter (pp_embed_spec_el fd m xd lookup) es @@ -88,7 +89,7 @@ and pp_embed_spec_el fd m xd lookup ese = output_string fd Grammar_pp.pp_DOUBLERIGHTBRACKET ) | Tex xo when (match ese with Embed_inner (_,"TEX_NAME_PREFIX")->true | _->false) -> output_string fd xo.ppt_name_prefix - | Tex _ | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> + | Tex _ | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> ( match ese with | Embed_string (l,s) -> output_string fd s diff --git a/src/grammar_pp.ml b/src/grammar_pp.ml index 6743c20..0c550a3 100644 --- a/src/grammar_pp.ml +++ b/src/grammar_pp.ml @@ -51,7 +51,7 @@ pp_plain_nonterm nt pp_nonterm m xd nt - gives a normal Ascii/Tex/Coq/Isa pp of nt, depending on the mode m + gives a normal Ascii/Tex/Coq/Lean/Isa pp of nt, depending on the mode m and syntax defn xd. This is only really sensible for nt which are known not to contain a suffix item of the form Si_index i. @@ -87,13 +87,14 @@ let pp_source_location m l = | Ascii _ | Tex _ -> Printf.sprintf "%% %s\n" s | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ -> Printf.sprintf "(* %s *)\n" s + | Lean _ -> Printf.sprintf "/- %s -/\n" s | Lex _ | Menhir _ -> "" (* utilities *********************************************************** *) -let list_append m = match m with | Lem _ | Hol _ -> " ++ " | _ -> " @ " +let list_append m = match m with | Lem _ | Hol _ | Lean _ -> " ++ " | _ -> " @ " let pad n s = let m = n - String.length s in @@ -884,13 +885,14 @@ and pp_dots m xd n = | 1 -> pp_tex_DOTDOTDOT | 2 -> pp_tex_DOTDOTDOTDOT | _ -> raise ThisCannotHappen ) - | Caml _ | Hol _ | Lem _ | Isa _ | Coq _ | Twf _ | Lex _ | Menhir _ -> + | Caml _ | Hol _ | Lem _ | Isa _ | Coq _ | Lean _ | Twf _ | Lex _ | Menhir _ -> raise ThisCannotHappen and pp_uninterpreted m xd s = match m with | Ascii ao -> col_cyan ao ("(*"^s^"*)") | Caml _ | Coq _ | Isa _ | Hol _ | Lem _ | Lex _ | Menhir _ -> "(*"^s^"*)" + | Lean _ -> "/-"^s^"-/" | Twf _ -> "%{"^s^"}%" | Tex _ -> let es = Auxl.pp_tex_escape s in @@ -900,13 +902,13 @@ and pp_uninterpreted m xd s = and pp_maybe_quote_ident m xd s = match m with | Ascii ao -> quote_ident s - | Tex _ | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> s + | Tex _ | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> s and pp_prod_flavour m xd pf = match m with | Ascii _ -> pp_BAR | Tex _ -> pp_tex_BAR - | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen + | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen and pp_plain_terminal tm = tm @@ -915,6 +917,7 @@ and pp_terminal m xd tm = | Ascii ao -> col_green ao (quote_ident tm) | Tex _ -> pp_tex_terminal m xd tm | Coq _ -> tm + | Lean _-> tm | Isa _ -> pp_isa_terminal m xd tm | Hol _ -> tm | Lem _ -> tm @@ -927,6 +930,7 @@ and pp_terminal_unquoted m xd tm = | Ascii ao -> col_green ao tm | Tex _ -> pp_tex_terminal m xd tm | Coq _ -> tm + | Lean _ -> tm | Isa _ -> pp_isa_terminal m xd tm | Hol _ -> tm | Lem _ -> tm @@ -1029,7 +1033,7 @@ and pp_nonterm_with_sie_internal as_type m xd sie (ntr,suff) = String.concat "" (apply_hom_spec m xd hs [Auxl.pp_tex_escape ntr^(pp_suffix_with_sie m xd sie suff)])) - | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> + | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> let s0 = pp_ntr ^ (pp_suffix_with_sie m xd sie suff) in let s1 = if as_type then s0 @@ -1078,7 +1082,7 @@ and pp_metavar_with_sie_internal as_type m xd sie (mvr,suff) = (apply_hom_spec m xd hs [Auxl.pp_tex_escape mvr^(pp_suffix_with_sie m xd sie suff)])) - | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> + | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> let s = pp_mvr ^ (pp_suffix_with_sie m xd sie suff) in if as_type then s else Auxl.hide_isa_trailing_underscore m s @@ -1092,7 +1096,7 @@ and pp_nt_or_mv_with_sie_internal as_type m xd sie (ntmv,suff) = and pp_nt_or_mv_with_de_with_sie_internal as_type m xd sie (de :dotenv) ((ntmvr,suff0) as ntmv) = match m with | Ascii _ | Tex _ -> pp_nt_or_mv_with_sie_internal as_type m xd sie ntmv - | Isa _ | Coq _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> + | Isa _ | Coq _ | Lean _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> let (de1,de2) = de in match try Some(List.assoc ntmv de2) with Not_found -> None with | None -> pp_nt_or_mv_with_sie m xd sie ntmv @@ -1116,6 +1120,17 @@ and pp_nt_or_mv_with_de_with_sie_internal as_type m xd sie (de :dotenv) ((ntmvr, | None -> "" | Some suffi -> " - "^pp_plain_suffix_item suffi) ^ ")))" + | Lean _ -> +leanTODO "1" ( + "((fun "^de1i.de1_pattern^" |-> "^pp_nt_or_mv_with_sie m xd ((Si_var ("_",0))::sie) (ntmvr,suff)^")" + ^ " (List.nth " ^ de1i.de1_compound_id ^ " " + ^ "(" ^ pp_plain_suffix_item suffi + ^ + (match non_zero_lower_of_bound bound with + | None -> "" + | Some suffi -> " - "^pp_plain_suffix_item suffi) + ^ ")))" +) | Hol _ -> " ((\\ "^de1i.de1_pattern^" . "^pp_nt_or_mv_with_sie m xd ((Si_var ("_",0))::sie) (ntmvr,suff)^")" ^ " (EL " ^ " " @@ -1317,6 +1332,13 @@ and pp_metavardefn m xd mvd = ^ " = " ^ pp_metavarrep m xd mvd.mvd_rep type_name mvd.mvd_loc ^ pp_com ^ "\n" + | Lean lno -> + let type_name = pp_metavarroot_ty m xd mvd.mvd_name in + "def " + ^ type_name + ^ " := " + ^ pp_metavarrep m xd mvd.mvd_rep type_name mvd.mvd_loc + ^ pp_com ^ "\n" | Twf _ -> "%abbrev " ^ pp_metavarroot_ty m xd mvd.mvd_name @@ -1346,6 +1368,11 @@ and pp_metavarrep m xd mvd_rep type_name loc = let hs = List.assoc "lem" mvd_rep in pp_hom_spec m xd hs with Not_found -> Auxl.warning (Some loc) ("undefined lem metavarrep for "^type_name^"\n"); "UNDEFINED" ) + | Lean lno -> + ( try + let hs = List.assoc "lean" mvd_rep in + pp_hom_spec m xd hs + with Not_found -> Auxl.warning (Some loc) ("undefined lean metavarrep for "^type_name^"\n"); "UNDEFINED" ) | Coq co -> ( try let hs = List.assoc "coq" mvd_rep in @@ -1402,6 +1429,7 @@ and pp_com_es m xd homs es = ^ "}" | Isa _ -> " \\ \\" ^ String.concat "" (apply_hom_spec m xd hs ss) ^ "\\" | Coq _ | Hol _ | Lem _ | Caml _ | Lex _ -> " (* " ^ String.concat "" (apply_hom_spec m xd hs ss) ^ " *)" + | Lean _ -> " /- " ^ String.concat "" (apply_hom_spec m xd hs ss) ^ " -/" | Menhir _ -> "/* " ^ String.concat "" (apply_hom_spec m xd hs ss) ^ " */" | Ascii _ | Twf _ -> "" @@ -1416,6 +1444,7 @@ and pp_com_strings m xd homs ss = ^ "}" | Isa _ -> " \\ \\" ^ String.concat "" (apply_hom_spec m xd hs ss) ^ "\\" | Coq _ | Hol _ | Lem _ | Caml _ | Lex _ -> " (* " ^ String.concat "" (apply_hom_spec m xd hs ss) ^ " *)" + | Lean _ -> " /- " ^ String.concat "" (apply_hom_spec m xd hs ss) ^ " -/" | Menhir _ -> "/* " ^ String.concat "" (apply_hom_spec m xd hs ss) ^ " */" | Ascii _ | Twf _ -> "" @@ -1434,7 +1463,7 @@ and pp_homomorphism m xd (hn,hs) = (* (\* raise ThisCannotHappen *\) *) (* | (Hol ho, "hol") -> (pp_hom_spec m xd hs)^"\n\n" *) (* (\* raise ThisCannotHappen *\) *) - | (Coq _, _) | (Isa _, _) | (Hol _,_) | (Lem _,_) | (Twf _,_) | (Caml _,_) | (Lex _,_) | (Menhir _, _) -> "" + | (Coq _, _) | (Lean _, _) | (Isa _, _) | (Hol _,_) | (Lem _,_) | (Twf _,_) | (Caml _,_) | (Lex _,_) | (Menhir _, _) -> "" | (Tex _, _) -> Auxl.errorm m "pp_homomorphism" and pp_homomorphism_list m xd homs = @@ -1442,7 +1471,7 @@ and pp_homomorphism_list m xd homs = | Ascii ao -> String.concat " " (List.map (pp_homomorphism m xd) homs) | Tex xo -> raise ThisCannotHappen - | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen + | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen and pp_hom_name m xd hn = pp_maybe_quote_ident m xd hn @@ -1473,7 +1502,7 @@ and pp_hom_spec_el m xd hse = | Hom_terminal s -> Auxl.errorm m "pp_hom_spec_el" | Hom_index i -> "UNIMPLEMENTED" | Hom_ln_free_index _ -> Auxl.errorm m "pp_hom_spec el") - | Isa _ | Hol _ | Lem _ -> + | Isa _ | Hol _ | Lem _ | Lean _ -> ( match hse with | Hom_string s -> s | Hom_terminal s -> s @@ -1538,7 +1567,7 @@ and pp_suffix_with_sie m xd sie suff = "_{" ^ String.concat "\\," (List.map (pp_suffix_item_with_sie m xd sie true) suff_subscript) ^ "}") - | (Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _) -> + | (Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _) -> (String.concat "" (List.map (pp_suffix_item_with_sie m xd sie false) suff)) @@ -1554,7 +1583,7 @@ and pp_suffix_item_with_sie m xd sie nosubscript suffi = ( (*List.nth sie i*) try List.nth sie i with Failure _ -> Si_num "999")) in if ao.ppa_ugly then "["^s^"]" else s - | (Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _) -> + | (Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _) -> ( match suffi with | Si_num s -> s | Si_punct s -> s @@ -1694,12 +1723,12 @@ and pp_bindspec m xd sie de bs = | Tex xo -> pp_tex_BIND ^ "\\; " ^ pp_mse_string m xd sie de mse ^ "\\; " ^ pp_tex_IN ^ "\\; " ^ pp_nonterm m xd nt - | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) + | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) | AuxFnDef (loc,f,mse) -> ( match m with | Ascii ao -> pp_auxfn m xd f ^ "" ^ pp_EQ ^ "" ^ pp_mse_string m xd sie de mse | Tex xo -> pp_auxfn m xd f ^ "" ^ pp_tex_EQ ^ "" ^ pp_mse_string m xd sie de mse - | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) + | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) | NamesEqual (loc,mse,mse') -> ( match m with | Ascii ao -> @@ -1710,7 +1739,7 @@ and pp_bindspec m xd sie de bs = pp_tex_NAMES ^ "" ^ pp_tex_LPAREN ^ "" ^ pp_mse_string m xd sie de mse ^ "" ^ pp_tex_RPAREN ^ "\\," ^ pp_tex_EQ ^ "\\," ^ pp_tex_NAMES ^ "" ^ pp_tex_LPAREN ^ "" ^ pp_mse_string m xd sie de mse' ^ "" ^ pp_tex_RPAREN - | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) + | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) | NamesDistinct (loc,mse,mse') -> ( match m with | Ascii ao -> @@ -1722,7 +1751,7 @@ and pp_bindspec m xd sie de bs = ^ ""^pp_tex_RPAREN ^ "\\," ^ pp_tex_HASH ^ "\\," ^ pp_tex_NAMES ^ "" ^ pp_tex_LPAREN ^ "" ^ pp_mse_string m xd sie de mse' ^ ""^pp_tex_RPAREN - | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) + | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) | AllNamesDistinct (loc,mse) -> ( match m with | Ascii ao -> @@ -1731,7 +1760,7 @@ and pp_bindspec m xd sie de bs = | Tex xo -> pp_tex_DISTINCTNAMES ^ "" ^ pp_tex_LPAREN ^ "" ^ pp_mse_string m xd sie de mse ^ "" ^ pp_tex_RPAREN - | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) + | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) and pp_bindspec_list m xd sie de bs = match m with @@ -1750,7 +1779,7 @@ and pp_bindspec_list m xd sie de bs = (* " $ \\\\ \n &&&& $ " *) (* (List.map (pp_bindspec m xd sie de) bs)) *) (* ^ (\* " $ & \\ $ " ^*\) pp_tex_BIND_RIGHT_DELIM ) *) - | Ascii _ | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen + | Ascii _ | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen and pp_plain_mse mse = match mse with @@ -1786,14 +1815,14 @@ and pp_mse m xd sie de isa_list_name_flag prod_name ntmvro mse : string * nonter ( match m with | Lex _ | Menhir _ -> Auxl.errorm m "pp_mse" | Ascii _ | Tex _ -> (* "\\{" ^*) pp_metavar_with_sie m xd sie mv (* ^ "\\}" *) - | Isa _ | Hol _ | Lem _ | Caml _ -> "["^pp_metavar_with_sie m xd sie mv^"]" + | Isa _ | Lean _ | Hol _ | Lem _ | Caml _ -> "["^pp_metavar_with_sie m xd sie mv^"]" | Coq _ -> "(cons " ^ pp_metavar_with_sie m xd sie mv ^ " nil)" | Twf _ -> "(natlist/cons " ^ pp_metavar_with_sie m xd sie mv ^ " natlist/nil)" ), [], [] | NonTermExp nt -> ( match m with | Lex _ | Menhir _ -> Auxl.errorm m "pp_mse" | Ascii _ | Tex _ -> (* "\\{" ^*) pp_nonterm_with_sie m xd sie nt (* ^ "\\}" *) - | Isa _ | Hol _ | Lem _ | Caml _ -> "["^pp_nonterm_with_sie m xd sie nt^"]" + | Isa _ | Lean _ | Hol _ | Lem _ | Caml _ -> "["^pp_nonterm_with_sie m xd sie nt^"]" | Coq _ -> "(cons " ^ pp_nonterm_with_sie m xd sie nt ^ " nil)" | Twf _ -> "(natlist/cons " ^ pp_nonterm_with_sie m xd sie nt ^ " natlist/nil)" ), [], [] | MetaVarListExp (mv,b) -> @@ -1852,7 +1881,7 @@ and pp_mse m xd sie de isa_list_name_flag prod_name ntmvro mse : string * nonter | Tex xo -> ( pp_auxfn m xd f ^ "" ^ pp_tex_LPAREN ^ "" ^ pp_nonterm_with_sie m xd sie nt ^ "" ^ pp_tex_RPAREN ), [], [] - | Isa _ | Coq _ | Hol _ | Lem _ | Twf _ | Caml _ -> + | Isa _ | Coq _ | Lean _ | Hol _ | Lem _ | Twf _ | Caml _ -> let ntrp = pp_nontermroot_ty m xd (Auxl.promote_ntr xd (Auxl.primary_ntr_of_ntr xd (fst nt))) in ( "(" ^ Auxl.auxfn_name f ntrp ntrp ^ " " ^ pp_nonterm_with_sie m xd sie nt^")" ), [], [] ) @@ -2033,6 +2062,7 @@ and pp_mse m xd sie de isa_list_name_flag prod_name ntmvro mse : string * nonter | Twf _ -> raise TwelfNotImplemented | Caml _ -> ( "(List.flatten (List.map "^Auxl.auxfn_name f ntrp ntrp ^" ("^pp_ntlist^")))" ), [], [] + | Lean _ -> (leanTODO "2" ( "(List.flatten (List.map "^Auxl.auxfn_name f ntrp ntrp ^" ("^pp_ntlist^")))" )), [], [] | Lem _ -> let ntrp_s = pp_nontermroot m xd ntrp in ( lemTODO "9" " (List.concat (List.map "^Auxl.auxfn_name f ntrp_s ntrp_s ^" ("^pp_ntlist^")))" ), [], [] @@ -2156,6 +2186,7 @@ and pp_mse m xd sie de isa_list_name_flag prod_name ntmvro mse : string * nonter f1 @ f2) | Caml _ -> ( pp_mse_string m xd sie de mse ^list_append m^ pp_mse_string m xd sie de mse' ), [], [] | Lem _ -> ( pp_mse_string m xd sie de mse ^list_append m^ pp_mse_string m xd sie de mse' ), [], [] + | Lean _ -> ( pp_mse_string m xd sie de mse ^list_append m^ pp_mse_string m xd sie de mse' ), [], [] | Hol _ -> ( "("^pp_mse_string m xd sie de mse ^list_append m^ pp_mse_string m xd sie de mse' ^")"), [], [] | Coq _ -> let (s1,d1,f1) = pp_mse m xd sie de isa_list_name_flag prod_name ntmvro mse in @@ -2169,7 +2200,7 @@ and pp_mse m xd sie de isa_list_name_flag prod_name ntmvro mse : string * nonter | Lex _ | Menhir _ -> Auxl.errorm m "pp_mse" | Ascii ao -> pp_EMPTY, [], [] | Tex xo -> pp_tex_EMPTY, [], [] - | Isa _ | Hol _ | Lem _ | Caml _ -> "[]", [], [] + | Isa _ | Lean _ | Hol _ | Lem _ | Caml _ -> "[]", [], [] | Coq _ -> "nil", [], [] | Twf _ -> "natlist/nil", [], [] ) @@ -2225,7 +2256,7 @@ and pp_element m xd sie in_type e = pp_tex_LEFTBRACKET ^ " " ^ String.concat " " (Auxl.option_map (pp_element m xd sie in_type) es) ^ " " ^ pp_tex_RIGHTBRACKET ) - | Coq _ | Caml _ | Hol _ | Lem _ | Twf _ | Isa _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) + | Coq _ | Lean _ | Caml _ | Hol _ | Lem _ | Twf _ | Isa _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) | Lang_sugaroption tm -> Some (pp_terminal m xd tm) | Lang_list elb -> @@ -2256,7 +2287,7 @@ and pp_element m xd sie in_type e = | Lang_sugaroption _ | Lang_list _ -> None) - | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ -> + | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ -> let check_conflict v t = if String.compare v t = 0 then Some "_", t @@ -2278,6 +2309,10 @@ and pp_element m xd sie in_type e = ( match pp_elements m xd sie es true false true true with | None -> None | Some s -> Some (None, "(option "^s^")") ) + | Lean _ -> + ( match pp_elements m xd sie es true false true true with + | None -> None + | Some s -> Some (None, "(option "^s^")") ) | Isa _ | Hol _ | Lem _ | Caml _ -> ( match pp_elements m xd sie es true false true true with | None -> None @@ -2298,6 +2333,10 @@ and pp_element m xd sie in_type e = ( match pp_elements m xd sie elb.elb_es true false true true with | None -> Some (None, "list unit") | Some s -> Some (None, "list "^s) ) + | Lean _ -> + ( match pp_elements m xd sie elb.elb_es true false true true with + | None -> Some (None, "list unit") + | Some s -> Some (None, "list "^s) ) | Isa _ | Hol _ -> ( match pp_elements m xd sie elb.elb_es true false true true with | None -> Some (None, "unit list") @@ -2331,7 +2370,7 @@ and pp_elements m xd sie es paren toplevel in_list in_type = match m with | Ascii _ | Tex _ | Lex _ | Menhir _ -> Some (String.concat " " (Auxl.option_map (pp_element m xd sie in_type) es) ) - | Coq _ | Caml _ | Lem _ -> + | Coq _ | Lean _ | Caml _ | Lem _ -> lemTODOmo m "10" (*really? *) ( let ss = (Auxl.option_map (pp_element m xd sie in_type) es) in let separator = @@ -2510,6 +2549,14 @@ and pp_prod m xd rnn rpw p = (* returns a string option *) if co.coq_names_in_rules then Some (" | " ^ p.prod_name ^ " " ^ s ^ pp_com) else Some (" | " ^ p.prod_name ^ " : " ^ s ^ " -> " ^ pp_nontermroot_ty m xd rnn ^ pp_com) ) + | Lean _ -> + if p.prod_meta then + None + else + ( match pp_elements m xd [] (apply_hom_order m xd p) (*p.prod_es*) false true false false with + | None -> Some (" | " ^ p.prod_name ^ " : " ^ pp_nontermroot_ty m xd rnn ^ pp_com) + | Some s -> + Some (" | " ^ p.prod_name ^ " : " ^ s ^ " -> " ^ pp_nontermroot_ty m xd rnn ^ pp_com) ) | Twf _ -> if p.prod_meta then None @@ -2629,7 +2676,7 @@ and pp_rule m xd r = (* returns a string option *) (pp_prod m xd r.rule_ntr_name r.rule_pn_wrapper) r.rule_ps)) ^ "") - | Hol _ | Lem _| Caml _ -> + | Hol _ | Lem _ | Lean _ | Caml _ -> if r.rule_meta || r.rule_phantom then None else @@ -2731,7 +2778,7 @@ and pp_rule_list m xd rs = (* and we generate a type abbreviation *) | [Ntr ntr] when (None<>Auxl.hom_spec_for_pp_mode m(Auxl.rule_of_ntr xd ntr).rule_homs - && match m with Isa _ | Coq _ | Hol _ | Lem _ | Caml _ -> true | _ -> false) + && match m with Isa _ | Coq _ | Lean _ | Hol _ | Lem _ | Caml _ -> true | _ -> false) -> (* PS hack to turn off printing of phantom nonterms which would otherwise turn into type abbreviations. Please check - maybe this should be before dependency analysis??? *) if (Auxl.rule_of_ntr xd ntr).rule_phantom then "" else @@ -2775,6 +2822,11 @@ and pp_rule_list m xd rs = ^ strip_surrounding_parens (pp_nontermroot_ty m xd ntr) ^ " = " ^ pp_hom_spec m xd hs ^ "\n\n" + | Lean _ -> + "\ndef " + ^ strip_surrounding_parens (pp_nontermroot_ty m xd ntr) ^ " := " + ^ pp_hom_spec m xd hs + ^ "\n\n" | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.errorm m "int_rule_list_dep" ) (* or not, in which case we generate an inductive type definition *) | b -> @@ -2818,6 +2870,11 @@ and pp_rule_list m xd rs = let coq_equality_code = !pp_internal_coq_buffer in pp_internal_coq_buffer := ""; def ^ coq_equality_code + | Lean _ -> + let def = int_rule_list_dep m xd rs (fun rs -> "\ninductive ") "\nwhere " "" in + (*let coq_equality_code = !pp_internal_coq_buffer in + pp_internal_coq_buffer := "";*) + def (*^ coq_equality_code*) | Twf wo -> int_rule_list_dep m xd rs (fun rs -> "") "\n" "" | Caml oo -> @@ -2962,7 +3019,7 @@ and pp_syntaxdefn m xd = ^ (if ao.ppa_show_deps then (pp_plain_top_sort m xd ^ pp_plain_dep_graph m xd) else "") - | Isa _ | Coq _ | Hol _ | Lem _ | Twf _ | Caml _ -> + | Isa _ | Coq _ | Lean _ | Hol _ | Lem _ | Twf _ | Caml _ -> String.concat "" (List.map (pp_metavardefn m xd) xd.xd_mds) ^ pp_rule_list m xd xd.xd_rs | Tex _ -> @@ -3008,6 +3065,12 @@ and pp_variable m xd mvrp var = (Auxl.mvd_of_mvr xd mvrp).mvd_rep with | None -> var | Some hs -> String.concat "" (apply_hom_spec m xd hs [var])) + | Lean _ -> + (match Auxl.hom_spec_for_hom_name + "leanvar" + (Auxl.mvd_of_mvr xd mvrp).mvd_rep with + | None -> var + | Some hs -> String.concat "" (apply_hom_spec m xd hs [var])) | Tex _ -> (match Auxl.hom_spec_for_hom_name "texvar" @@ -3172,7 +3235,7 @@ and pp_symterm_node_body m xd sie de stnb : string = let include_terminals = match m with | Ascii _ | Tex _ | Lex _ | Menhir _ -> true - | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ -> false + | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ -> false | Caml oo -> oo.ppo_include_terminals in let pp_es' () = pp_symterm_elements' m xd sie de include_terminals prod_es stnb.st_es in let pp_es () = pp_symterm_elements m xd sie de include_terminals prod_es stnb.st_es in @@ -3183,7 +3246,7 @@ and pp_symterm_node_body m xd sie de stnb : string = ( match stnb.st_prod_name with | "formula_dots" -> String.concat " \\quad " (pp_es()) | _ -> pp_tex_insert_spacing (pp_es'())) - | Isa _ | Hol _ | Lem _ | Coq _ | Twf _ | Caml _ -> + | Isa _ | Hol _ | Lem _ | Coq _ | Lean _ | Twf _ | Caml _ -> ( match stnb.st_prod_name with (* special case pp for proof assistant judgement forms *) @@ -3201,7 +3264,9 @@ and pp_symterm_node_body m xd sie de stnb : string = | Some(hs,arity,prec) -> pp_symterm_element_judge_isa_fancy m xd sie de hs p'' stnb'') | Coq co -> - pp_symterm_element_judge_coq_plain m xd sie de p'' stnb'' + pp_symterm_element_judge_coq_plain m xd sie de p'' stnb'' + | Lean lno -> + pp_symterm_element_judge_lean_plain m xd sie de p'' stnb'' | Twf wo -> pp_symterm_element_judge_twf_plain m xd sie de p'' stnb'' | Hol ho -> @@ -3273,6 +3338,17 @@ and pp_symterm_node_body m xd sie de stnb : string = ^ ")" ) ) + | Lean _ -> + ( match stnb.st_es with + | [] -> stnb.st_prod_name + | _ -> + leanTODO "3" ( + "(" + ^ "List.all (fun b |-> b)" ^ " " + ^ String.concat " " (pp_es()) + ^ ")" + ) + ) | Coq co -> let dl = ("formula: " ^(String.concat " -- " @@ -3491,7 +3567,7 @@ and pp_symterm_node_body m xd sie de stnb : string = ^ String.concat "" (apply_hom_spec m xd hs (pp_es())) ^")") - | Coq _ | Twf _ -> + | Coq _ | Lean _ | Twf _ -> ( match stnb.st_es with | [] -> promoted_pn | _ -> @@ -3568,6 +3644,11 @@ and pp_symterm_element_judge_coq_plain m xd sie de p'' stnb'' = stnb''.st_prod_name ^ " " ^ String.concat " " pp_es'' +and pp_symterm_element_judge_lean_plain m xd sie de p'' stnb'' = + let pp_es'' = pp_symterm_elements m xd sie de false p''.prod_es stnb''.st_es in + stnb''.st_prod_name ^ " " + ^ String.concat " " pp_es'' + and pp_symterm_element_judge_hol_plain m xd sie de p'' stnb'' = let pp_es'' = pp_symterm_elements m xd sie de false p''.prod_es stnb''.st_es in " ( " @@ -3647,7 +3728,7 @@ and pp_symterm_list_items m xd sie (de :dotenv) tmopt prod_es stlis : (string * let include_terminals = match m with | Ascii _ | Tex _ | Lex _ | Menhir _ -> true - | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ -> false + | Coq _ | Lean _ | Isa _ | Hol _ | Lem _ | Twf _ -> false | Caml oo -> oo.ppo_include_terminals in let tmopt' = ( match tmopt with @@ -3660,6 +3741,7 @@ and pp_symterm_list_items m xd sie (de :dotenv) tmopt prod_es stlis : (string * | Isa _ -> ["[]",TTC_dummy] | Caml _ -> ["[]",TTC_dummy] | Lem _ -> ["[]",TTC_dummy] + | Lean _ -> ["[]",TTC_dummy] | Coq co -> if co.coq_expand_lists then ["Nil_list_"^(String.concat "_" (elements_to_string prod_es)),TTC_dummy ] @@ -3676,7 +3758,7 @@ and pp_symterm_list_items m xd sie (de :dotenv) tmopt prod_es stlis : (string * Auxl.list_concat tmopt' (List.map (pp_symterm_list_item m xd sie de tmopt include_terminals prod_es) stlis) in (match m with Ascii ao when ao.ppa_ugly -> [col_magenta ao "[slb",TTC_dummy] @ ss @ [col_magenta ao "slb]",TTC_dummy] | _ -> ss) - | Isa _ | Caml _ | Coq _ | Hol _ | Lem _ | Twf _ -> + | Isa _ | Caml _ | Coq _ | Lean _ | Hol _ | Lem _ | Twf _ -> let pp_stlis = List.map (function xs->List.map fst xs) (List.map (pp_symterm_list_item m xd sie de tmopt include_terminals prod_es) stlis) in (List.map (function s -> (s,TTC_dummy)) (match m with @@ -3704,6 +3786,12 @@ and pp_symterm_list_items m xd sie (de :dotenv) tmopt prod_es stlis : (string * (Auxl.list_concat [ "++" ] pp_stlis) ^ ")")] + | Lean _ -> + [ leanTODO "4" ("(" + ^ String.concat " " + (Auxl.list_concat [ "++" ] + pp_stlis) + ^ ")")] | Coq co -> (* FZ use Auxl.list_app_coq *) let l = List.flatten @@ -3745,7 +3833,7 @@ and pp_symterm_list_item m xd sie (de :dotenv) tmopt include_terminals prod_es s (match m with | Ascii ao -> if ao.ppa_ugly then [col_magenta ao "[stli_single",TTC_dummy] @ pp_es' @ [col_magenta ao "stli_single]",TTC_dummy] else pp_es' | Tex _ -> pp_es' - | Caml _ | Isa _ | Hol _ | Lem _ -> + | Caml _ | Isa _ | Hol _ | Lem _ | Lean _ -> ["[(" ^ String.concat "," pp_es ^ ")]",TTC_dummy] | Coq co -> if co.coq_expand_lists then @@ -3845,11 +3933,11 @@ and pp_symterm_list_body m xd sie (de :dotenv) tmopt include_terminals prod_es s ^ "}",TTC_comp] ) - | Isa _ | Coq _ | Hol _ | Lem _ | Twf _ | Caml _ -> + | Isa _ | Coq _ | Lean _ | Hol _ | Lem _ | Twf _ | Caml _ -> (List.map (function s -> (s,TTC_dummy)) (match m with | Ascii _ | Tex _ | Lex _ | Menhir _ -> raise ThisCannotHappen - | Isa _ | Coq _ | Hol _ | Lem _ | Twf _ | Caml _ -> + | Isa _ | Coq _ | Lean _ | Hol _ | Lem _ | Twf _ | Caml _ -> (* interim placeholder code - not remotely right *) (* FZ I hope that this comment is outdated *) let es = stlb.stl_elements in @@ -3899,7 +3987,11 @@ and pp_symterm_list_body m xd sie (de :dotenv) tmopt include_terminals prod_es s ^ de1i.de1_compound_id ^ ")"] | Lem _ -> - [lemTODO "14" ("(List.map (fun "^de1i.de1_pattern^" -> "^pp_body^") " + [lemTODO "7" ("(List.map (fun "^de1i.de1_pattern^" -> "^pp_body^") " + ^ de1i.de1_compound_id + ^ ")")] + | Lean _ -> + [leanTODO "5" ("(List.map (fun "^de1i.de1_pattern^" -> "^pp_body^") " ^ de1i.de1_compound_id ^ ")")] | Coq co -> @@ -4282,6 +4374,7 @@ let pp_pp_mode m = match m with | Isa _ -> "Isa" | Hol _ -> "Hol" | Lem _ -> "Lem" + | Lean _ -> "Lean" | Twf _ -> "Twf" | Ascii _ -> "Ascii" | Tex _ -> "Tex" diff --git a/src/grammar_typecheck.ml b/src/grammar_typecheck.ml index 48c1b59..3783191 100644 --- a/src/grammar_typecheck.ml +++ b/src/grammar_typecheck.ml @@ -404,30 +404,30 @@ let subrule (xd:syntaxdefn) (include_meta_prods:bool) let allowable_hom_data = [ - ( Hu_root , (["isa";"coq";"hol";"lem";(*"twf";*)"tex";"ocaml"], + ( Hu_root , (["isa";"coq";"lean";"hol";"lem";(*"twf";*)"tex";"ocaml"], "nonterminal, metavar or indexvar root")); - ( Hu_metavar , (["isa";"coq";"hol";"lem";(*"twf";*)"tex";"ocaml";"com";"coq-equality";"coq-notation";"coq-universe";"lex";"texvar";"isavar";"holvar";"lemvar";"ocamlvar";"repr-locally-nameless";(*"repr-nominal";*)"phantom";"ocamllex";"ocamllex-remove";"ocamllex-of-string";"pp";"pp-raw";"pp-suppress"], + ( Hu_metavar , (["isa";"coq";"lean";"hol";"lem";(*"twf";*)"tex";"ocaml";"com";"coq-equality";"coq-notation";"coq-universe";"lex";"texvar";"isavar";"holvar";"lemvar";"leanvar";"ocamlvar";"repr-locally-nameless";(*"repr-nominal";*)"phantom";"ocamllex";"ocamllex-remove";"ocamllex-of-string";"pp";"pp-raw";"pp-suppress"], "metavar declaration")); - ( Hu_rule , (["isa";"coq";"hol";"lem";(*"twf";*)"tex";"ocaml";"com";"coq-equality";"coq-notation";"coq-universe";(*"icht";*)"icho";"ichlo";"ich";"ichl";"ic";"ch";"ih";"phantom";"aux";"auxparam";"menhir-start";"menhir-start-type";"quotient-with";"pp";"pp-raw";"pp-suppress";"pp-params";"lex-comment"], + ( Hu_rule , (["isa";"coq";"lean";"hol";"lem";(*"twf";*)"tex";"ocaml";"com";"coq-equality";"coq-notation";"coq-universe";(*"icht";*)"icho";"ichlo";"ich";"ichl";"ic";"ch";"ih";"phantom";"aux";"auxparam";"menhir-start";"menhir-start-type";"quotient-with";"pp";"pp-raw";"pp-suppress";"pp-params";"lex-comment"], "rule")); ( Hu_rule_meta, (["com"], "special rule")); - ( Hu_prod , (["isa";"coq";"hol";"lem";(*"twf";*)"tex";"texlong";"ocaml";"com";"order";"isasyn";"isaprec";(*"icht";*)"icho";"ichlo";"ich";"ichl";"ic";"ch";"ih"; + ( Hu_prod , (["isa";"coq";"lean";"hol";"lem";(*"twf";*)"tex";"texlong";"ocaml";"com";"order";"isasyn";"isaprec";(*"icht";*)"icho";"ichlo";"ich";"ichl";"ic";"ch";"ih"; "disambiguate";"prec";"leftassoc";"rightassoc";"menhir";"quotient-remove";"menhir-prec";"pp";"pp-raw"], "production")); ( Hu_prod_tm , (["isa"; "tex";"lex"; "com"; "prec";"leftassoc";"rightassoc"],"production of the terminals grammar")); ( Hu_drule , ([ "com"],"definition rule")); ( Hu_defn , ([ "tex"; "com";"isasyn";"isaprec";"disambiguate";"lemwcf"],"definition")); ( Hu_defnclass, (["coq-universe"],"defns block")); - ( Hu_fundefn , (["isa";"coq";"hol";"lem";(*"twf";*)"tex"; "com";"order";"isasyn";"isaprec";(*"icht";*)"icho";"ichlo";"ich";"ichl";"ic";"ch";"ih";"coq-struct"],"function definition")); + ( Hu_fundefn , (["isa";"coq";"lean";"hol";"lem";(*"twf";*)"tex"; "com";"order";"isasyn";"isaprec";(*"icht";*)"icho";"ichlo";"ich";"ichl";"ic";"ch";"ih";"coq-struct"],"function definition")); ( Hu_fundefnclass, ([(* "isa-proof";*)"hol-proof"],"funs block")); ( Hu_subrule, (["isa-proof"],"subrule definition")); ( Hu_subst, (["isa-proof"],"substitution definition")); ( Hu_freevar, (["isa-proof";"isa-set"],"free variable definition")); - (* ( Hu_embed , (["isa";"coq";"hol";"lem";(\*"twf";*\)"tex";"ocaml";"isa-auxfn-proof";"isa-subrule-proof"],"embed section")); *) + (* ( Hu_embed , (["isa";"coq";"lean";"hol";"lem";(\*"twf";*\)"tex";"ocaml";"isa-auxfn-proof";"isa-subrule-proof"],"embed section")); *) ( Hu_deadcode, ([], "Internal error: Hu_deadcode")); ] -let embed_allowable_homs = ["coq";"coq-lib";"coq-preamble"; +let embed_allowable_homs = ["coq";"lean";"coq-lib";"coq-preamble";"lean-preamble"; "isa";"isa-import";"isa-auxfn-proof";"isa-subrule-proof";"isa-lib";"isa-preamble"; "hol";"hol-preamble"; "lem";"lem-preamble"; @@ -436,7 +436,7 @@ let embed_allowable_homs = ["coq";"coq-lib";"coq-preamble"; "ocaml";"ocaml-preamble"; "menhir"] -let list_form_allowable_homs =["isa";"coq";"hol";"lem";"ic";"ch";"ih";"ich";"ichl";"icho";"ichlo";(*"icht";*)"coq-struct";"ocaml"] +let list_form_allowable_homs =["isa";"coq";"lean";"hol";"lem";"ic";"ch";"ih";"ich";"ichl";"icho";"ichlo";(*"icht";*)"coq-struct";"ocaml"] let cd_disambiguate_hom name rhs hs = try @@ -818,6 +818,7 @@ and cd_prod c (rn:string) (pnw:string) (targets:string list) (rule_homs_for_targ (fun h -> match h with Hom_index _ -> true | _ -> false) (List.assoc "order" homs) in let oh_coq = ( "coq", (Hom_string ("("^prod_name))::oh@[Hom_string ")"] ) in + let oh_lean= ( "lean", (Hom_string ("("^prod_name))::oh@[Hom_string ")"] ) in let oh_isa = ( "isa", (Hom_string ("("^prod_name))::oh@[Hom_string ")"] ) in let oh_hol = let of_s = if List.length oh = 0 then "" else " of " in @@ -826,7 +827,7 @@ and cd_prod c (rn:string) (pnw:string) (targets:string list) (rule_homs_for_targ (* let oh_lem = ( "lem", (Hom_string ("("^prod_name))::bracket_commas oh @[Hom_string ")"] ) in *) let oh_lem = ( "lem", (Hom_string ("("^prod_name))::oh@[Hom_string ")"] ) in (* LemTODO25: *) - homs @ [oh_coq; oh_isa; oh_hol; oh_caml; oh_lem] + homs @ [oh_coq; oh_lean; oh_isa; oh_hol; oh_caml; oh_lem] with Not_found -> homs in let cd_order_funmeta prod_name homs elems = @@ -842,12 +843,13 @@ and cd_prod c (rn:string) (pnw:string) (targets:string list) (rule_homs_for_targ elems)) [] in let oh_coq = ( "coq", (Hom_string ("("^prod_name))::oh@[Hom_string ")"] ) in + let oh_lean= ( "lean", (Hom_string ("("^prod_name))::oh@[Hom_string ")"] ) in let oh_isa = ( "isa", (Hom_string ("("^prod_name))::oh@[Hom_string ")"] ) in let oh_hol = ( "hol", (Hom_string ("("^prod_name))::oh@[Hom_string ")"] ) in let oh_lem = ( "lem", (Hom_string ("("^prod_name))::oh@[Hom_string ")"] ) in let oh_caml= ( "ocaml", (Hom_string ("("^prod_name))::oh @[Hom_string ")"] ) in let oh_ord = ( "order", oh ) in - List.filter (fun x -> fst x <> "order") homs @ [oh_coq; oh_lem; oh_isa; oh_hol; oh_caml; oh_ord] + List.filter (fun x -> fst x <> "order") homs @ [oh_coq; oh_lean; oh_lem; oh_isa; oh_hol; oh_caml; oh_ord] in let es = cd_elements c p.raw_prod_es in let hu = if rn="terminals" then Hu_prod_tm else Hu_prod in @@ -1931,7 +1933,7 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b r.raw_rule_homs) in let rule_homs = if r.raw_rule_ntr_name = "formula" then - [("coq", [Hom_string "Prop"]); ("hol", [Hom_string "bool"]); + [("coq", [Hom_string "Prop"]); ("lean", [Hom_string "Prop"]); ("hol", [Hom_string "bool"]); ("lem", [Hom_string "bool"]); ("isa", [Hom_string "bool"]); ("ocaml", [Hom_string "bool"])] else rule_homs in @@ -1966,6 +1968,7 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b | "tex-wrap-pre" | "tex-wrap-post" -> Some (l,hn,he) | "coq-preamble" -> Some (l,"coq",he) + | "lean-preamble" -> Some (l,"lean",he) | "isa-preamble" -> Some (l,"isa",he) | "hol-preamble" -> Some (l,"hol",he) | "lem-preamble" -> Some (l,"lem",he) diff --git a/src/main.ml b/src/main.ml index 0c67e50..cbfb482 100644 --- a/src/main.ml +++ b/src/main.ml @@ -59,6 +59,9 @@ let lem_filter_filename_dsts = ref ([] : string list) let coq_filter_filenames = ref ([] : (string * string) list) let coq_filter_filename_srcs = ref ([] : string list) let coq_filter_filename_dsts = ref ([] : string list) +let lean_filter_filenames = ref ([] : (string * string) list) +let lean_filter_filename_srcs = ref ([] : string list) +let lean_filter_filename_dsts = ref ([] : string list) let twf_filter_filenames = ref ([] : (string * string) list) let twf_filter_filename_srcs = ref ([] : string list) let twf_filter_filename_dsts = ref ([] : string list) @@ -128,6 +131,10 @@ let options = Arg.align [ Arg.Tuple[Arg.String (fun s -> coq_filter_filename_srcs := s :: !coq_filter_filename_srcs); Arg.String (fun s -> coq_filter_filename_dsts := s :: !coq_filter_filename_dsts)], " Files to Coq filter" ); + ( "-lean_filter", + Arg.Tuple[Arg.String (fun s -> lean_filter_filename_srcs := s :: !lean_filter_filename_srcs); + Arg.String (fun s -> lean_filter_filename_dsts := s :: !lean_filter_filename_dsts)], + " Files to Lean filter" ); ( "-hol_filter", Arg.Tuple[Arg.String (fun s -> hol_filter_filename_srcs := s :: !hol_filter_filename_srcs); Arg.String (fun s -> hol_filter_filename_dsts := s :: !hol_filter_filename_dsts)], @@ -318,6 +325,7 @@ let _ = hol_filter_filenames := List.combine (!hol_filter_filename_srcs) (!hol_f let _ = lem_filter_filenames := List.combine (!lem_filter_filename_srcs) (!lem_filter_filename_dsts) let _ = isa_filter_filenames := List.combine (!isa_filter_filename_srcs) (!isa_filter_filename_dsts) let _ = coq_filter_filenames := List.combine (!coq_filter_filename_srcs) (!coq_filter_filename_dsts) +let _ = lean_filter_filenames := List.combine (!lean_filter_filename_srcs) (!lean_filter_filename_dsts) let _ = twf_filter_filenames := List.combine (!twf_filter_filename_srcs) (!twf_filter_filename_dsts) let _ = caml_filter_filenames := List.combine (!caml_filter_filename_srcs) (!caml_filter_filename_dsts) @@ -325,6 +333,7 @@ let types_of_extensions = [ "ott","ott"; "tex","tex"; "v", "coq"; + "lean", "lean"; "thy","isa"; "sml","hol"; "lem","lem"; @@ -345,7 +354,7 @@ let file_type name = with _ -> None -let non_tex_output_types = ["coq"; "isa"; "hol"; "lem"; "twf"; "ocaml"] +let non_tex_output_types = ["coq"; "lean"; "isa"; "hol"; "lem"; "twf"; "ocaml"] let output_types = "tex" :: "lex" :: "menhir" :: non_tex_output_types let input_types = "ott" :: output_types @@ -373,7 +382,7 @@ let classify_file_argument arg = (* *) (* values, containing first all the ott source files from the end of *) (* the command line, if any, then all the explicit -in and -out arguments, *) -(* and finally any -tex/-coq/-hol/-isabelle/-lem/-ocaml arguments *) +(* and finally any -tex/-coq/-lean/-hol/-isabelle/-lem/-ocaml arguments *) let all_file_arguments = List.map classify_file_argument (List.rev (!file_arguments)) @@ -392,7 +401,7 @@ let targets_in ts = let targets_non_tex = targets_in non_tex_output_types let targets = targets_in output_types -let targets_for_non_picky = targets_in [(*"lex";"ocaml";*)"hol";"lem";"isa";"twf";"coq";"tex"] +let targets_for_non_picky = targets_in [(*"lex";"ocaml";*)"hol";"lem";"isa";"twf";"coq";"lean";"tex"] (* collect the source filenames *) let source_filenames = @@ -424,6 +433,7 @@ let m_isa = Isa { ppi_isa_primrec = !isa_primrec; ppi_generate_lemmas = !isa_generate_lemmas } let m_hol = Hol { hol_library = ref ("",[]); } let m_lem = Lem { lem_library = ref ("",[]); } +let m_lean = Lean { lean_library = ref ("",[]); } let m_twf = Twf { twf_current_defn = ref ""; twf_library = ref ("",[]) } let m_coq = Coq { coq_expand_lists = !coq_expand_lists; @@ -527,6 +537,7 @@ let _ = "isa",m_isa; "twf",m_twf; "coq",m_coq ; + "lean",m_lean ; "tex",m_tex ]) targets_for_non_picky) @@ -774,6 +785,8 @@ let output_stage (sd,lookup,sd_unquotiented,sd_quotiented_unaux) = System_pp.pp_systemdefn_core_io m_hol sd lookup fi !merge_fragments | "lem" -> System_pp.pp_systemdefn_core_io m_lem sd lookup fi !merge_fragments + | "lean" -> + System_pp.pp_systemdefn_core_io m_lean sd lookup fi !merge_fragments | "twf" -> System_pp.pp_systemdefn_core_io m_twf sd lookup fi !merge_fragments | "ocaml" -> @@ -856,6 +869,7 @@ let output_stage (sd,lookup,sd_unquotiented,sd_quotiented_unaux) = (List.iter (filter m_tex) (!tex_filter_filenames)); (List.iter (filter m_coq) (!coq_filter_filenames)); + (List.iter (filter m_lean) (!lean_filter_filenames)); (List.iter (filter m_isa) (!isa_filter_filenames)); (List.iter (filter m_hol) (!hol_filter_filenames)); (List.iter (filter m_lem) (!lem_filter_filenames)); diff --git a/src/subrules_pp.ml b/src/subrules_pp.ml index 002ccec..45d6487 100644 --- a/src/subrules_pp.ml +++ b/src/subrules_pp.ml @@ -308,6 +308,10 @@ let pp_subrules m xd srs : int_funcs_collapsed = [ lemTODO "15" (" (List.all (fun "^de1i.de1_pattern^" -> "^conjuncted_conjuncts^") " ^ de1i.de1_compound_id ^ ")")], deps, [] + | Lean _ -> + [ leanTODO "7" (" (List.all (fun "^de1i.de1_pattern^" => "^conjuncted_conjuncts^") " + ^ de1i.de1_compound_id + ^ ")")], deps, [] | Coq co when not co.coq_expand_lists -> let e = if List.length (Str.split (Str.regexp "(\\|,\\|)") de1i.de1_pattern) = 1 @@ -424,7 +428,7 @@ let pp_subrules m xd srs : int_funcs_collapsed = dep := deps @ !dep; funcs := !funcs @ new_funcs; match m with - | Coq _ | Hol _ | Lem _| Isa _ | Caml _ -> + | Coq _ | Lean _ | Hol _ | Lem _| Isa _ | Caml _ -> if conjuncts = [] then Auxl.pp_true m false else String.concat (Auxl.pp_and m false) conjuncts @@ -434,7 +438,7 @@ let pp_subrules m xd srs : int_funcs_collapsed = pls in match m with - | Coq _ | Hol _ | Lem _ | Isa _ | Caml _ -> + | Coq _ | Lean _ | Hol _ | Lem _ | Isa _ | Caml _ -> let rhs = if rhss = [] then Auxl.pp_false m false @@ -484,6 +488,18 @@ let pp_subrules m xd srs : int_funcs_collapsed = " : " ^ (if co.coq_expand_lists then "Prop :=\n" else "bool :=\n") ^ " match " ^ Grammar_pp.pp_nonterm m xd fresh_var ^ " with\n" ) + | Lean _ -> + let nts_used = Context_pp.nts_used_in_lhss m xd ru in +(* let nts_used = Auxl.nts_used_in_rule ru in *) + let fresh_var_ntr = Auxl.secondary_ntr xd sru in + let fresh_var = Auxl.fresh_nt nts_used (fresh_var_ntr,[]) in (* FZ Substs_pp *) + ( Auxl.pp_is srl sru + ^ " (" ^ Grammar_pp.pp_nonterm m xd fresh_var + ^ ":" ^ Grammar_pp.pp_nontermroot_ty m xd sru ^ ")", + "", + " : " + ^ ("bool :=\n") + ^ " match " ^ Grammar_pp.pp_nonterm m xd fresh_var ^ " with\n" ) | Twf _ -> ( Auxl.pp_is srl sru ^ " : " ^ Grammar_pp.pp_nontermroot_ty m xd sru diff --git a/src/substs_pp.ml b/src/substs_pp.ml index 6ab8213..be304f0 100644 --- a/src/substs_pp.ml +++ b/src/substs_pp.ml @@ -146,12 +146,12 @@ let pp_list_all_cong_lemma_isa = let pp_list_mem m = match m with | Coq co -> Auxl.add_to_lib co.coq_library "list_mem" pp_list_mem_coq - | Caml _ | Hol _ | Lem _ | Isa _ | Tex _ | Twf _ | Ascii _ | Lex _ | Menhir _ + | Caml _ | Hol _ | Lem _ | Lean _ | Isa _ | Tex _ | Twf _ | Ascii _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_list_mem" let pp_list_filter m = match m with | Coq co -> Auxl.add_to_lib co.coq_library "list_filter" pp_list_filter_coq - | Isa _ | Hol _ | Lem _ | Caml _ | Tex _ | Twf _ | Ascii _ | Lex _ | Menhir _ + | Isa _ | Hol _ | Lem _ | Lean _ | Caml _ | Tex _ | Twf _ | Ascii _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_list_filter" let pp_list_minus m = match m with @@ -159,6 +159,7 @@ let pp_list_minus m = match m with | Lem oo -> Auxl.add_to_lib oo.lem_library "list_minus" pp_list_minus_lem | Isa io -> Auxl.add_to_lib io.isa_library "list_minus" pp_list_minus_isa | Hol ho -> () + | Lean lno -> () | Coq co -> pp_list_mem m; Auxl.add_to_lib co.coq_library "list_minus" pp_list_minus_coq @@ -168,12 +169,13 @@ let pp_list_minus2 m = match m with | Coq co -> pp_list_mem m; Auxl.add_to_lib co.coq_library "list_minus2" pp_list_minus2_coq - | Caml _ | Hol _ | Lem _ | Isa _ | Twf _ | Tex _ | Ascii _ | Lex _ | Menhir _ + | Caml _ | Hol _ | Lem _ | Lean _ | Isa _ | Twf _ | Tex _ | Ascii _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_list_minus2" let pp_list_assoc m = match m with | Isa io -> Auxl.add_to_lib io.isa_library "list_assoc" pp_list_assoc_isa | Hol ho -> () + | Lean lno -> () | Lem lo -> Auxl.add_to_lib lo.lem_library "list_assoc" pp_list_assoc_lem | Coq co -> Auxl.add_to_lib co.coq_library "list_assoc" pp_list_assoc_coq | Caml _ | Twf _ | Tex _ | Ascii _ | Lex _ | Menhir _ @@ -320,6 +322,16 @@ let pp_auxfn_clauses m xd f ntr ntmvr = "", " : list " ^ Grammar_pp.pp_nt_or_mv_root_ty m xd ntmvr ^ " :=\n" ^ " match " ^ Grammar_pp.pp_nonterm m xd pat_var ^ " with\n" ) + | Lean _ -> + let nts_used = Context_pp.nts_used_in_lhss m xd (Auxl.rule_of_ntr xd ntr) in + let fresh_var_ntr = Auxl.secondary_ntr xd ntr in + let pat_var = Auxl.fresh_nt nts_used (fresh_var_ntr,[]) in + ( (leanTODO "8" (Auxl.auxfn_name f ntrn ntrn (* FZ *) + ^ " (" ^ Grammar_pp.pp_nonterm m xd pat_var + ^ ":" ^ Grammar_pp.pp_nontermroot_ty m xd ntr ^ ")")), + "", + " : list " ^ Grammar_pp.pp_nt_or_mv_root_ty m xd ntmvr ^ " :=\n" + ^ " match " ^ Grammar_pp.pp_nonterm m xd pat_var ^ " where\n" ) | Lem _ | Caml _ -> let nts_used = Context_pp.nts_used_in_lhss m xd (Auxl.rule_of_ntr xd ntr) in @@ -593,6 +605,11 @@ let rec pp_subst_symterm ^ that_s ^ " " ^ "(" ^ Grammar_pp.pp_mse_string m xd sie de bound_things_glommed ^ ")" + | Lean _ -> + leanTODO "9" " List.elem " + ^ that_s + ^ " " + ^ "(" ^ Grammar_pp.pp_mse_string m xd sie de bound_things_glommed ^ ")" | Coq _ -> pp_list_mem m; "list_mem " @@ -667,6 +684,22 @@ let rec pp_subst_symterm ^ nt_s ^ ")" ) + | Lean _ -> + leanTODO "10" ( + "(" + ^ Auxl.subst_name subst.sb_name dep_name ^ " " + ^ (match bound_things_glommed with + | Empty -> sub_var + | _ -> + "(List.filter " + ^ "(fun ("^ that_s ^","^ this_s ^") |-> " + ^ "not("^that_in_bound_things()^")" + ^ ")" + ^ " "^sub_var^")") + ^ " " + ^ nt_s + ^ ")" + ) | Coq co -> "(" ^ Auxl.subst_name subst.sb_name dep_name ^ " " @@ -927,6 +960,7 @@ and pp_subst_symterm_list_body ("", "Cons_"^suf^" "^lp^" "^rp, "Cons_"^suf^" " ^ rhs ^ " (" ^ id ^ " " ^ common_lhs ^ " "^rp^")" ) ] } ]) + | Lean _ -> (leanTODO "11" "",[]) | Caml _ -> ("",[]) @@ -1052,6 +1086,18 @@ and pp_subst_symterm_list_body ^ de1i.de1_compound_id ^ ")", [] ) + | Lean _ -> + let l = Str.split (Str.regexp "(\\|,\\|)") de1i.de1_pattern in + if List.length l = 1 then + ( leanTODO "12" ("(List.map (fun ("^de1i.de1_pattern^":" ^ de1i.de1_coq_type_of_pattern ^ ") |-> "^pp_body^") " + ^ de1i.de1_compound_id + ^ ")"), [] ) + else + ( leanTODO "13" ("(List.map (fun (pat_:" ^ de1i.de1_coq_type_of_pattern ^ ") |-> match pat_ with " (* FZ freshen pat_ *) + ^ de1i.de1_pattern^" => " ^pp_body^" ) " + ^ de1i.de1_compound_id + ^ ")"), [] ) + | Caml _ -> ( "(List.map (fun "^de1i.de1_pattern^" -> "^pp_body^") " ^ de1i.de1_compound_id @@ -1086,7 +1132,7 @@ let pp_subst_prod let lhs_pat = Grammar_pp.pp_symterm m xd sie de lhs_st in let lhs = ( match m with - | Coq _ | Caml _ | Lem _ -> lhs_pat + | Coq _ | Lean _ | Caml _ | Lem _ -> lhs_pat | Isa _ | Hol _ | Twf _ -> (* Auxl.subst_name subst.sb_name rule_ntr_name ^ " " *) ( if subst.sb_multiple then sub_var @@ -1149,6 +1195,19 @@ let pp_subst_prod ^ " -> " ^ Grammar_pp.pp_nonterm m xd this_var ^ " end)" ) + | Lean _ -> + pp_list_assoc m; + (* tentative hol code for multiple subst *) + leanTODO "14" ( + "(match list_assoc_option " + ^ thing_s ^ " " + ^ sub_var + ^ " with " + ^ "| Nothing => " ^ lhs_pat + ^ "| Just " ^ Grammar_pp.pp_nonterm m xd this_var + ^ " => " ^ Grammar_pp.pp_nonterm m xd this_var + ^ " )" + ) | Coq coq_opt -> pp_list_assoc m; "(match list_assoc " (* A B eq *) @@ -1176,7 +1235,7 @@ let pp_subst_prod let that_s = Grammar_pp.pp_nt_or_mv m xd that_var in let eq_s = ( match m with - | Isa _ | Hol _ | Lem _ | Caml _ -> thing_s ^ "=" ^ that_s + | Isa _ | Hol _ | Lem _ | Lean _ | Caml _ -> thing_s ^ "=" ^ that_s | Twf _ -> raise Auxl.ThisCannotHappen | Coq _ -> ( if Auxl.require_locally_nameless xd @@ -1389,6 +1448,23 @@ let pp_subst_rule : subst -> pp_mode -> syntaxdefn -> nontermroot list -> rule - " {struct " ^ Grammar_pp.pp_nonterm m xd in_var ^"}", " : " ^ Grammar_pp.pp_nontermroot_ty m xd r.rule_ntr_name ^ " :=\n" ^ " match " ^ Grammar_pp.pp_nonterm m xd in_var ^ " with\n" ) ) + | Lean _ -> + ( (id + ^ ( if subst.sb_multiple + then + (leanTODO "15" (" (" ^ sub_var ^ ":list (" + ^ Grammar_pp.pp_nt_or_mv_root_ty m xd subst.sb_that + ^ "*" ^ Grammar_pp.pp_nontermroot_ty m xd subst.sb_this ^ "))" )) + else + (leanTODO "16" ( " (" ^ Grammar_pp.pp_nonterm m xd this_var ^ ":" + ^ Grammar_pp.pp_nontermroot_ty m xd subst.sb_this ^")" + ^ " (" ^ Grammar_pp.pp_nt_or_mv m xd that_var ^ ":" + ^ Grammar_pp.pp_nt_or_mv_root_ty m xd subst.sb_that ^ ")" ) + ^ " (" ^ Grammar_pp.pp_nonterm m xd in_var ^ ":" + ^ Grammar_pp.pp_nontermroot_ty m xd r.rule_ntr_name ^")"))), + " {struct " ^ Grammar_pp.pp_nonterm m xd in_var ^"}", + " : " ^ Grammar_pp.pp_nontermroot_ty m xd r.rule_ntr_name ^ " :=\n" + ^ " match " ^ Grammar_pp.pp_nonterm m xd in_var ^ " with\n" ) | Lem _ | Caml _ -> @@ -1541,7 +1617,7 @@ let rec pp_fv_symterm let call = Auxl.fv_name fv.fv_name id (* (Auxl.promote_ntr xd ntrp) *) ^ " " ^ nt_s in ( match m with | Twf _ -> Some call - | Isa _ | Hol _ | Lem _ | Caml _ | Coq _ -> Some ("("^call^")") + | Isa _ | Hol _ | Lem _ | Caml _ | Coq _ | Lean _ -> Some ("("^call^")") | Tex _ | Ascii _ | Lex _ | Menhir _ -> assert false)) else None in @@ -1575,13 +1651,13 @@ let rec pp_fv_symterm | Isa _ when has_isa_set_hom fv -> "(" ^ s ^ " - set " ^ Grammar_pp.pp_mse_string m xd sie de bound_things_glommed ^")" - | Isa _ | Hol _ | Lem _ | Caml _ | Coq _ -> + | Isa _ | Hol _ | Lem _ | Caml _ | Coq _ | Lean _ -> pp_list_minus m; "(list_minus " ^ (match m with (* HACK is the name eq_thing always correct? *) | Ascii _ | Tex _ | Twf _ | Lex _ | Menhir _ -> Auxl.errorm m "list_minus" - | Isa _ | Hol _ | Lem _ | Caml _ -> "" + | Isa _ | Hol _ | Lem _ | Lean _ | Caml _ -> "" | Coq _ -> "eq_" ^ (Grammar_pp.pp_nt_or_mv_root_ty m xd fv.fv_that) ^ " " ) ^ s ^" " ^ Grammar_pp.pp_mse_string m xd sie de bound_things_glommed ^")") ) @@ -1622,7 +1698,7 @@ and pp_fv_symterm_element then Some (match m with - | Isa _ | Hol _ | Lem _ | Caml _ -> ("["^mv_s^"]") + | Isa _ | Hol _ | Lem _ | Lean _ | Caml _ -> ("["^mv_s^"]") | Coq _ -> ("(cons "^mv_s^" nil)") | Twf _ -> ("(natlist/cons "^mv_s^" natlist/nil)") | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_fv_symterm_element" @@ -1717,7 +1793,7 @@ and pp_fv_symterm_list_body (* TODO optimise the output in the common case of a list of singletons *) match m with | Twf _ | Tex _ | Ascii _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_fv_symterm_list_body" - | Isa _ | Coq _ | Hol _ | Lem _ | Caml _ -> + | Isa _ | Coq _ | Lean _ | Hol _ | Lem _ | Caml _ -> let pp_body_elements, funcs = let body_options, funcs = List.split @@ -1731,7 +1807,7 @@ and pp_fv_symterm_list_body let body_elements = let tmp = ( match m with - | Coq _ -> Auxl.insert_append m pp_body_elements + | Coq _ | Lean _ -> Auxl.insert_append m pp_body_elements | Isa _ when has_isa_set_hom fv -> String.concat " \\ " pp_body_elements | _ -> String.concat (list_append m) pp_body_elements ) in if List.length pp_body_elements = 1 @@ -1826,6 +1902,12 @@ and pp_fv_symterm_list_body ("(List.concat (List.map (fun "^de1i.de1_pattern^" -> "^pp_body^") " ^ de1i.de1_compound_id ^ "))"), funcs + | Lean _ -> + let pp_body = String.concat (leanTODO "17" " ++ ") pp_body_elements in + Some + ("(List.concat (List.map (fun "^de1i.de1_pattern^" -> "^pp_body^") " + ^ de1i.de1_compound_id + ^ "))"), funcs | Coq co when co.coq_expand_lists -> let var_list = Str.split (Str.regexp "(\\|,\\|)") de1i.de1_pattern in let args = @@ -1903,7 +1985,7 @@ let pp_freevar_prod let rhs = (match m with | Isa _ when (List.exists (fun (x,_) -> x = "isa-set") fv.fv_homs) -> "{"^thing_s^"}" - | Isa _ | Hol _ | Lem _ | Caml _ -> ("["^thing_s^"]") + | Isa _ | Hol _ | Lem _ | Lean _ | Caml _ -> ("["^thing_s^"]") | Coq co -> if not !(co.coq_locally_nameless) then "(cons "^thing_s^" nil)" @@ -1950,7 +2032,7 @@ let pp_freevar_prod | [] -> (match m with | Isa _ when has_isa_set_hom fv -> "{}" - | Isa _ | Hol _ | Lem _ | Caml _ -> "[]" + | Isa _ | Hol _ | Lem _ | Lean _ | Caml _ -> "[]" | Coq co -> if not !(co.coq_locally_nameless) then "nil" @@ -1960,7 +2042,7 @@ let pp_freevar_prod | _ -> ( match m with | Isa _ when has_isa_set_hom fv -> String.concat " \\ " rhs_elements - | Isa _ | Caml _ | Lem _ -> String.concat (list_append m) rhs_elements + | Isa _ | Caml _ | Lem _ | Lean _ -> String.concat (list_append m) rhs_elements | Hol _ -> String.concat " ++ " rhs_elements | Coq co -> if not !(co.coq_locally_nameless) @@ -2032,6 +2114,22 @@ let pp_freevar_rule : freevar -> pp_mode -> syntaxdefn -> nontermroot list -> ru | Lem _ -> " list " ^ Grammar_pp.pp_nt_or_mv_root_ty m xd fv.fv_that ) ^ " =\n match " ^ Grammar_pp.pp_nonterm m xd fresh_var ^ " with\n" + + | Lean _ -> + let nts_used = Context_pp.nts_used_in_lhss m xd r in + let fresh_var_ntr = Auxl.secondary_ntr xd r.rule_ntr_name in + let fresh_var = Auxl.fresh_nt nts_used (fresh_var_ntr,[]) in + let ntrn = Grammar_pp.pp_nontermroot m xd r.rule_ntr_name in + + lemTODOm m "24" ( + Auxl.fv_name fv.fv_name ntrn (* r.rule_ntr_name *) + ^ " (" ^ Grammar_pp.pp_nonterm m xd fresh_var + ^ ":" ^ Grammar_pp.pp_nontermroot_ty m xd r.rule_ntr_name + ^ ") "), + "", + ": " + ^ " list " ^ Grammar_pp.pp_nt_or_mv_root_ty m xd fv.fv_that + ^ " =\n match " ^ Grammar_pp.pp_nonterm m xd fresh_var ^ " where\n" | Twf _ -> ( Auxl.fv_name fv.fv_name r.rule_ntr_name ^ " : " diff --git a/src/system_pp.ml b/src/system_pp.ml index 88f3b2e..9598d8c 100644 --- a/src/system_pp.ml +++ b/src/system_pp.ml @@ -77,6 +77,7 @@ let pp_functions_locally_nameless fd m sd xd_transformed = | Hol ho -> fst (!(ho.hol_library)) | Lem lo -> fst (!(lo.lem_library)) | Coq co -> fst (!(co.coq_library)) + | Lean lno -> fst (!(lno.lean_library)) | Twf wo -> fst (!(wo.twf_library)) | Caml oo-> fst (!(oo.caml_library)) | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_functions") in @@ -151,6 +152,7 @@ let pp_functions fd m sd lookup = | Isa io -> fst (!(io.isa_library)) | Hol ho -> fst (!(ho.hol_library)) | Lem lo -> fst (!(lo.lem_library)) + | Lean lno -> fst (!(lno.lean_library)) | Coq co -> fst (!(co.coq_library)) | Twf wo -> fst (!(wo.twf_library)) | Caml oo ->fst (!(oo.caml_library)) @@ -187,6 +189,7 @@ let pp_library fd m = | Isa io -> pp_lib io.isa_library | Hol ho -> pp_lib ho.hol_library | Lem lo -> pp_lib lo.lem_library + | Lean lno -> pp_lib lno.lean_library | Coq co -> pp_lib co.coq_library | Twf wo -> pp_lib wo.twf_library | Caml oo-> pp_lib oo.caml_library @@ -378,6 +381,9 @@ let pp_systemdefn fd m sd lookup fn = Printf.fprintf fd "val _ = new_theory \"%s\";\n" fn; pp_systemdefn_core fd m sd lookup; output_string fd "\nval _ = export_theory ();\n" + | Lean lno -> + Printf.fprintf fd "/- generated by Ott %s from: %s -/\n" Version.n sd.sources; + pp_systemdefn_core fd m sd lookup | Coq co -> (* FZ keeping for now locally_nameless repr separated from the main *) if Auxl.require_locally_nameless sd.syntax @@ -481,6 +487,15 @@ let pp_systemdefn_core_io m sd lookup oi merge_fragments = | true -> ["Arith"; "Bool"; "List"] | false -> ["Arith"; "Bool"; "List"; "Ott.ott_list_core"])) ^ "\n\n" )] + | Lean lno -> + [ Embed_string (dummy_loc, + "/- generated by Ott " ^ Version.n ^ " from: " ^ file_sources ^ " -/\n\n" +(* ^ String.concat "\n" (List.map (fun th -> "Require Import " ^ th ^ ".") + ( match co.coq_expand_lists with + | true -> ["Arith"; "Bool"; "List"] + | false -> ["Arith"; "Bool"; "List"; "Ott.ott_list_core"])) +*) + ^ "\n\n" )] | Twf wo -> [ Embed_string (dummy_loc, "%% generated by Ott "^Version.n^" from: "^file_sources^" \n" )] diff --git a/src/types.ml b/src/types.ml index f770b73..1962eb5 100644 --- a/src/types.ml +++ b/src/types.ml @@ -816,6 +816,8 @@ and pp_coq_opts = coq_lngen : bool; coq_use_filter_fn : bool; coq_names_in_rules : bool } (* co *) +and pp_lean_opts = + { lean_library : (string * string list) ref } (* lno *) and pp_isa_opts = { ppi_isa_primrec : bool; ppi_isa_inductive : bool; @@ -859,6 +861,7 @@ type pp_yacc_opts = unit (* yo *) type pp_mode = (* m *) | Coq of pp_coq_opts + | Lean of pp_lean_opts | Isa of pp_isa_opts | Hol of pp_hol_opts | Lem of pp_lem_opts @@ -963,6 +966,12 @@ let lemTODOm m s1 s2 = match m with Lem _ -> lemTODO s1 s2 | _ -> s2 let lemTODOmo m s1 s2o = match s2o with None -> None | Some s2 -> Some (lemTODOm m s1 s2) +(** ************************ *) +(** lean debug *) +(** ************************ *) +let lean_debug = ref false +let leanTODO s1 s2 = if !lean_debug then "(* leanTODO "^s1^"*) "^s2 else s2 + (* from grammar_typecheck *) From 77b86f4f5445aa1fe99bd89011467890eae5caaa Mon Sep 17 00:00:00 2001 From: Peter Sewell Date: Sun, 15 Feb 2026 09:01:37 +0000 Subject: [PATCH 2/5] minimal working lean backend sketch. It generates well-typed Lean for examples/1Bsemantics/l1.ott; probably not for anything else --- examples/1Bsemantics/l1.ott | 60 ++++++++++++++++++++++++------------- src/defns.ml | 33 +++++++++++++------- src/dependency.ml | 25 ++++++++++++++++ src/grammar_pp.ml | 17 +++++++++-- src/grammar_typecheck.ml | 2 +- src/subrules_pp.ml | 2 +- 6 files changed, 103 insertions(+), 36 deletions(-) diff --git a/examples/1Bsemantics/l1.ott b/examples/1Bsemantics/l1.ott index c41f609..00b285b 100644 --- a/examples/1Bsemantics/l1.ott +++ b/examples/1Bsemantics/l1.ott @@ -1,26 +1,41 @@ +embed {{ lean +set_option linter.unusedVariables false + +open Option +}} + metavar n ::= {{ com Numeric literals }} {{ phantom }} {{ lex numeric }} {{ lem integer }} {{ coq someZarithtype }} + {{ lean Int }} -metavar location, l ::= +metavar Location {{ lean Location }}, l ::= {{ com Store locations }} {{ lem string }} {{ coq somestringtype }} + {{ lean String }} + {{ lean-equality }} + +% think idiomatic Lean to capitalise that, but with `metavar location {{ lean Location }}` it hits a bug in which the lean hom isn't respected in the inductive rule printing, so I've just capitalised the metavar for now - which will probably be bad for other targets grammar -b :: 'B_' ::= {{ com booleans }} {{ phantom }} {{ lem bool }} {{ coq bool }} - | true :: :: true {{ lem true }} {{ coq true }} - | false :: :: false {{ lem false }} {{ coq false }} +b :: 'B_' ::= {{ com booleans }} {{ phantom }} {{ lem bool }} {{ coq bool }} {{ lean Bool }} + | true :: :: true {{ lem true }} {{ coq true }} {{ lean true }} + | false :: :: false {{ lem false }} {{ coq false }} {{ lean false }} -operations, op :: 'Op_' ::= {{ com operations }} +% is it nice to deeply embed the L1 bools like this or not? + +operations {{ lean Operations }}, op :: 'op_' ::= {{ com operations }} | + :: :: plus | >= :: :: gteq -e :: 'E_' ::= {{ com expressions }} +% all the other languages have constructors capitalised, but in Lean it seems conventional to have them lower-case. Ott doesn't support per-target constructor name prefixes, so in this file I've lower-cased them all for now. + +expr {{ lean Expr }}, e :: 'e_' ::= {{ com expressions }} | n :: :: num | b :: :: bool | e1 op e2 :: :: op @@ -37,11 +52,14 @@ v :: 'V_' ::= {{ com values }} | b :: :: bool | skip :: :: skip -store , s :: 'Store_' ::= {{ com stores }} {{ phantom }} {{ lem list (location * integer) }} {{ coq list (location * integer) }} - | empty :: :: empty {{ lem [] }} {{ coq [] }} - | s , l |-> n :: :: extend {{ lem (([[l]],[[n]])::[[s]]) }} {{ coq (([[l]],[[n]])::[[s]]) }} +store {{ lean Store }}, s :: 'store_' ::= {{ com stores }} {{ phantom }} {{ lem list (Location * integer) }} {{ coq list (Location * integer) }} {{ lean List (Location × Int) }} + | empty :: :: empty {{ lem [] }} {{ coq [] }} {{ lean [] }} + | s , l |-> n :: :: extend {{ lem (([[l]],[[n]])::[[s]]) }} {{ coq (([[l]],[[n]])::[[s]]) }} {{ lean (([[l]],[[n]])::[[s]]) }} + +config {{ lean Config }}, c :: 'Config_' ::= {{ com configurations }} {{ phantom }} {{lem (expr*store) }} {{ coq (expr * store) }} {{ lean ([[Expr]] × [[Store]]) }} + | < e , s > :: :: config {{ lem ([[e]], [[s]]) }} {{ coq ([[e]], [[s]]) }} {{ lean ([[e]], [[s]]) }} -typ, T :: 'T_' ::= {{ com types }} +typ {{ lean Typ }}, T :: 't_' ::= {{ com types }} | int :: :: int | bool :: :: bool | unit :: :: unit @@ -50,12 +68,12 @@ Tloc {{ isa tloc }} {{ coq tloc }} {{ hol tloc }} {{ lem tloc }} {{ ocaml tloc } | intref :: :: intref -type_assumption, ta :: 'TA_' ::= {{ com type assumption }} - | l : Tloc :: :: loc +type_assumption {{ lean Type_assumption }}, ta :: 'TA_' ::= {{ com type assumption }} {{ lean ([[Location]]×[[Tloc]]) }} + | l : Tloc :: :: loc {{ lean ([[l]], [[Tloc]]) }} -G {{ tex \Gamma }} :: G_ ::= {{ com type environments }} {{ phantom }} {{ lem list type_assumption }} {{ coq list type_assumption }} - | empty :: :: empty {{ lem [] }} {{ coq [] }} - | G , ta :: :: extend {{ lem ([[ta]]::[[G]]) }} {{ coq ([[ta]]::[[G]]) }} +G {{ tex \Gamma }} :: G_ ::= {{ com type environments }} {{ phantom }} {{ lem list type_assumption }} {{ coq list type_assumption }} {{ lean (List Type_assumption) }} + | empty :: :: empty {{ lem [] }} {{ coq [] }} {{ lean [] }} + | G , ta :: :: extend {{ lem ([[ta]]::[[G]]) }} {{ coq ([[ta]]::[[G]]) }} {{ lean ([[ta]]::[[G]]) }} terminals :: terminals_ ::= @@ -74,13 +92,13 @@ subrules grammar formula :: formula_ ::= | judgement :: :: judgement - | n1 + n2 = n3 :: :: sum {{ lem ([[n1]]+[[n2]]=[[n3]]) }} {{ coq ([[n1]]+[[n2]]=[[n3]]) }} - | n1 >= n2 = b :: :: leq {{ lem ([[n1]]>=[[n2]]=[[b]]) }} {{ coq ([[n1]]>=[[n2]]=[[b]]) }} - | s ( l ) = n :: :: lookup {{ lem (List.lookup [[l]] [[s]] =Just ([[n]])) }} {{ coq (List.lookup [[l]] [[s]] =Just ([[n]])) }} - | G ( l ) = Tloc :: :: type_lookup {{ lem (lookup_location_type [[l]] [[G]] = Just ([[Tloc]])) }} {{ coq (lookup_location_type [[l]] [[G]] = Just ([[Tloc]])) }} + | n1 + n2 = n3 :: :: sum {{ lem ([[n1]]+[[n2]]=[[n3]]) }} {{ coq ([[n1]]+[[n2]]=[[n3]]) }} {{ lean ([[n1]]+[[n2]]=[[n3]]) }} + | n1 >= n2 = b :: :: leq {{ lem ([[n1]]>=[[n2]]=[[b]]) }} {{ coq ([[n1]]>=[[n2]]=[[b]]) }} {{ lean (([[n1]]>=[[n2]])=[[b]]) }} + | s ( l ) = n :: :: lookup {{ lem (List.lookup [[l]] [[s]] =Just ([[n]])) }} {{ coq (List.lookup [[l]] [[s]] =Some ([[n]])) }} {{ lean (List.lookup [[l]] [[s]] = some ([[n]])) }} + | G ( l ) = Tloc :: :: type_lookup {{ lem (lookup_location_type [[l]] [[G]] = Just ([[Tloc]])) }} {{ coq (lookup_location_type [[l]] [[G]] = Some ([[Tloc]])) }} {{ lean (List.lookup [[l]] [[G]] = some ([[Tloc]])) }} -% this is a bit ugly - to capture the different use of Gamma in L1 and L2 we have a list of a Lem variant type and two special-purpose lookup functions, with a wildcard pattern match in each. +% this is a bit ugly - to capture the different use of Gamma in L1 and L2 we have a list of a Lem variant type and two special-purpose lookup functions, with a wildcard pattern match in each. Not currently implemented for Lean. embed {{ lem let rec lookup_location_type l g = @@ -98,7 +116,7 @@ Jop :: '' ::= % Reductions. Want to allow lem hom to specify witness and animation info defn -< e , s > -> < e' , s' > :: :: reduce :: '' {{ com $\langle[[e]],\,[[s]]\rangle$ reduces to $\langle[[e']],\,[[s']]\rangle$ }} by +c -> c' :: :: reduce :: '' {{ com $\langle[[e]],\,[[s]]\rangle$ reduces to $\langle[[e']],\,[[s']]\rangle$ }} by n1 + n2 = n ---------------------- :: op_plus diff --git a/src/defns.ml b/src/defns.ml index e3f9dac..3dd8808 100644 --- a/src/defns.ml +++ b/src/defns.ml @@ -412,7 +412,7 @@ let pp_drule fd (m:pp_mode) (xd:syntaxdefn) (dr:drule) : unit = Printf.fprintf fd "%s%s%s: " (leanTODO "18" "") "" (*("(*"^Location.pp_loc dr.drule_loc^"*)")*) - dr.drule_name; + ("| " ^ dr.drule_name); (* Lem currrently requires a forall even if there are no quantified variables, and a "true ==>" if there are no premises *) (* @@ -421,25 +421,26 @@ let pp_drule fd (m:pp_mode) (xd:syntaxdefn) (dr:drule) : unit = | _ -> *) output_string fd "forall"; - List.iter (fun (var,ty,_) -> Printf.fprintf fd " %s" (leanTODO "19" var)) +(* the second version, with explicit type annotations, is pretty noisy, and probably not idiomatic. For l1.ott, we need it only for b:bool, where Lean type inference seems to get confused? *) +(* List.iter (fun (var,ty,_) -> Printf.fprintf fd " %s" (leanTODO "19" var)) quantified_proof_assistant_vars; -(* List.iter (fun (var,ty,_) -> Printf.fprintf fd " (%s:%s)" var ty) - quantified_proof_assistant_vars;*) - output_string fd " .\n"; +*) List.iter (fun (var,ty,_) -> Printf.fprintf fd " (%s:%s)" var ty) + quantified_proof_assistant_vars; + output_string fd ",\n"; (* ); *) if (snd ppd_premises)<>[] || ppd_subntrs<>[] then begin (* output_string fd " &&\n(";*) - iter_asep fd " /\\n" + iter_asep fd " ->\n" (fun s -> output_string fd "("; output_string fd s; output_string fd ")") (ppd_subntrs @ snd ppd_premises); output_string fd "\n" end else output_string fd "true\n"; - output_string fd " ==> \n"; + output_string fd " -> \n"; output_string fd ppd_conclusion; output_string fd "\n\n" @@ -527,8 +528,20 @@ let pp_defn fd (m:pp_mode) (xd:syntaxdefn) lookup (defnclass_wrapper:string) (un Printf.fprintf fd "(* defn %s *)\n\n" d.d_name; iter_sep (pp_processed_semiraw_rule fd m xd) "and\n" d.d_rules | Lean _ -> - Printf.fprintf fd "/- defn %s -/\n\n" d.d_name; - iter_sep (pp_processed_semiraw_rule fd m xd) (leanTODO "20" "and\n") d.d_rules + (*Printf.fprintf fd "/- defn %s -/\n\n" d.d_name;*) + + let prod_name = defnclass_wrapper ^ d.d_name in + + let type_defn = + let es = (Auxl.prod_of_prodname xd prod_name).prod_es in + let ss = (Auxl.option_map (Grammar_pp.pp_element m xd [] true) es) in + match ss with + | [] -> universe^" :=" + | [s] -> s ^ " -> "^universe^" :=" + | _ -> String.concat " -> " ss ^ " -> " ^ universe^" where" in + Printf.fprintf fd "%s%s : %s /- defn %s -/\n" defnclass_wrapper d.d_name type_defn d.d_name; + iter_nosep (fun psr -> pp_processed_semiraw_rule fd m xd "" psr) d.d_rules + | Coq co -> (* FZ factor this code ? *) let prod_name = defnclass_wrapper ^ d.d_name in @@ -673,7 +686,7 @@ let pp_defnclass fd (m:pp_mode) (xd:syntaxdefn) lookup (dc:defnclass) = | Lean co -> Printf.fprintf fd "\n/- defns %s -/\ninductive " dc.dc_name; - iter_asep fd "\nwhere " + iter_asep fd "\ninductive " (fun d -> pp_defn fd m xd lookup dc.dc_wrapper universe d) dc.dc_defns diff --git a/src/dependency.ml b/src/dependency.ml index 9b1a7a2..1ffd9fe 100644 --- a/src/dependency.ml +++ b/src/dependency.ml @@ -531,6 +531,15 @@ let coq_collapse m xd funcs = (f.r_fun_id, f.r_fun_dep, (f.r_fun_header, (collapse_clauses m f.r_fun_id f.r_fun_clauses), Footer_empty)) in List.map (collapse_func m) funcs.i_funcs +let lean_collapse m xd funcs = + let collapse_clause m id (_,lhs, rhs) = + " | " ^ lhs ^ " => " ^ rhs ^ "\n" in + let collapse_clauses m id clauses = + String.concat "" (List.map (collapse_clause m id) clauses) in + let collapse_func m f = + (f.r_fun_id, f.r_fun_dep, (f.r_fun_header, (collapse_clauses m f.r_fun_id f.r_fun_clauses), Footer_empty)) in + List.map (collapse_func m) funcs.i_funcs + let twf_collapse m xd funcs = let collapse_clause m id (pfx, lhs, rhs) = "" ^ id ^ "/" ^ pfx ^ " : " ^ id ^ " " ^ lhs ^ " " ^ rhs ^ ".\n" in @@ -574,6 +583,7 @@ let collapse m xd (funcs:int_funcs) : int_funcs_collapsed = | Hol _ -> hol_collapse m xd funcs | Lem _ -> lem_collapse m xd funcs | Coq _ -> coq_collapse m xd funcs + | Lean _ -> lean_collapse m xd funcs | Twf _ -> twf_collapse m xd funcs | Caml _ -> caml_collapse m xd funcs | Tex _ | Ascii _ -> Auxl.error None "internal: collapse of Tex-Ascii\n" @@ -668,6 +678,21 @@ let print m xd (sorting,refl) = ^ "end.\n\n" in String.concat "" (List.map print_block sorting) + | Lean _ -> + let print_block block = + if ((List.length block) = 1) + then + let (nt,((h1,h2,h3),s,_)) = List.hd block in + if (List.mem nt refl) + then "def " ^ h1 ^ h2 ^ h3 ^ s ^ "\n\n" + else "def " ^ h1 ^ h3 ^ s ^ (if String.compare h3 "" = 0 then "\n\n" else "\n\n") + else + "def " + ^ (String.concat "\nwith " + (List.map (fun (_,((h1,h2,h3),s,_)) -> h1 ^ h2 ^ h3 ^ s) block)) + ^ "\n\n" in + leanTODO "21" (String.concat "" (List.map print_block sorting)) + | Twf _ -> (* PLACEHOLDER CODE *) let print_block block = diff --git a/src/grammar_pp.ml b/src/grammar_pp.ml index 0c550a3..f192de4 100644 --- a/src/grammar_pp.ml +++ b/src/grammar_pp.ml @@ -1339,6 +1339,13 @@ and pp_metavardefn m xd mvd = ^ " := " ^ pp_metavarrep m xd mvd.mvd_rep type_name mvd.mvd_loc ^ pp_com ^ "\n" + ^ (match + try Some (List.assoc "lean-equality" mvd.mvd_rep) with Not_found -> None + with + | None -> "" + | Some eh -> "deriving instance BEq for " ^ type_name ^ "\n" + ) + | Twf _ -> "%abbrev " ^ pp_metavarroot_ty m xd mvd.mvd_name @@ -2681,9 +2688,9 @@ and pp_rule m xd r = (* returns a string option *) then None else Some - (strip_surrounding_parens (pp_nontermroot_ty m xd r.rule_ntr_name) ^ " = "^pp_com^"\n" + (strip_surrounding_parens (pp_nontermroot_ty m xd r.rule_ntr_name) ^ (match m with Lean _ -> " where" | _ -> " := ")^pp_com^"\n" ^ (match m with Lem _ -> " | " | _ -> " ") - ^ String.concat " | " + ^ String.concat (match m with Lean _ -> " " | _ -> " | ") (List.map (function s -> s^"\n") (Auxl.option_map @@ -2872,9 +2879,13 @@ and pp_rule_list m xd rs = def ^ coq_equality_code | Lean _ -> let def = int_rule_list_dep m xd rs (fun rs -> "\ninductive ") "\nwhere " "" in + let lean_equality_code = + "open " ^ String.concat " " (Auxl.option_map (fun r -> if r.rule_meta || r.rule_phantom || (try (List.assoc "lean" r.rule_homs);true with Not_found -> false) then None else Some (pp_nontermroot_ty m xd r.rule_ntr_name)) rs) ^ "\n" in + (*let coq_equality_code = !pp_internal_coq_buffer in pp_internal_coq_buffer := "";*) - def (*^ coq_equality_code*) + def ^ (*^ coq_equality_code*) + lean_equality_code | Twf wo -> int_rule_list_dep m xd rs (fun rs -> "") "\n" "" | Caml oo -> diff --git a/src/grammar_typecheck.ml b/src/grammar_typecheck.ml index 3783191..b8ac520 100644 --- a/src/grammar_typecheck.ml +++ b/src/grammar_typecheck.ml @@ -406,7 +406,7 @@ let allowable_hom_data = [ ( Hu_root , (["isa";"coq";"lean";"hol";"lem";(*"twf";*)"tex";"ocaml"], "nonterminal, metavar or indexvar root")); - ( Hu_metavar , (["isa";"coq";"lean";"hol";"lem";(*"twf";*)"tex";"ocaml";"com";"coq-equality";"coq-notation";"coq-universe";"lex";"texvar";"isavar";"holvar";"lemvar";"leanvar";"ocamlvar";"repr-locally-nameless";(*"repr-nominal";*)"phantom";"ocamllex";"ocamllex-remove";"ocamllex-of-string";"pp";"pp-raw";"pp-suppress"], + ( Hu_metavar , (["isa";"coq";"lean";"hol";"lem";(*"twf";*)"tex";"ocaml";"com";"coq-equality";"coq-notation";"coq-universe";"lean-equality";"lex";"texvar";"isavar";"holvar";"lemvar";"leanvar";"ocamlvar";"repr-locally-nameless";(*"repr-nominal";*)"phantom";"ocamllex";"ocamllex-remove";"ocamllex-of-string";"pp";"pp-raw";"pp-suppress"], "metavar declaration")); ( Hu_rule , (["isa";"coq";"lean";"hol";"lem";(*"twf";*)"tex";"ocaml";"com";"coq-equality";"coq-notation";"coq-universe";(*"icht";*)"icho";"ichlo";"ich";"ichl";"ic";"ch";"ih";"phantom";"aux";"auxparam";"menhir-start";"menhir-start-type";"quotient-with";"pp";"pp-raw";"pp-suppress";"pp-params";"lex-comment"], "rule")); diff --git a/src/subrules_pp.ml b/src/subrules_pp.ml index 45d6487..4a6ab2d 100644 --- a/src/subrules_pp.ml +++ b/src/subrules_pp.ml @@ -498,7 +498,7 @@ let pp_subrules m xd srs : int_funcs_collapsed = ^ ":" ^ Grammar_pp.pp_nontermroot_ty m xd sru ^ ")", "", " : " - ^ ("bool :=\n") + ^ ("Bool :=\n") ^ " match " ^ Grammar_pp.pp_nonterm m xd fresh_var ^ " with\n" ) | Twf _ -> ( Auxl.pp_is srl sru ^ " : " From a0318630dcd55758afa12121131caf376caaeeb7 Mon Sep 17 00:00:00 2001 From: Peter Sewell Date: Sun, 15 Feb 2026 14:14:19 +0000 Subject: [PATCH 3/5] name constructor arguments in Lean output --- examples/1Bsemantics/l1.ott | 6 ++++-- src/grammar_pp.ml | 4 ++++ 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/examples/1Bsemantics/l1.ott b/examples/1Bsemantics/l1.ott index 00b285b..0de14a4 100644 --- a/examples/1Bsemantics/l1.ott +++ b/examples/1Bsemantics/l1.ott @@ -86,6 +86,8 @@ terminals :: terminals_ ::= | < :: :: la {{ tex \langle }} | > :: :: ra {{ tex \rangle }} +% for proof, would one really want subrules to generate functions, as Ott does, or more inductive relations? + subrules v <:: e @@ -116,7 +118,7 @@ Jop :: '' ::= % Reductions. Want to allow lem hom to specify witness and animation info defn -c -> c' :: :: reduce :: '' {{ com $\langle[[e]],\,[[s]]\rangle$ reduces to $\langle[[e']],\,[[s']]\rangle$ }} by +c -> c' :: :: Reduce :: '' {{ com $\langle[[e]],\,[[s]]\rangle$ reduces to $\langle[[e']],\,[[s']]\rangle$ }} by n1 + n2 = n ---------------------- :: op_plus @@ -168,7 +170,7 @@ c -> c' :: :: reduce :: '' {{ com $\langle[[e]],\,[[s]]\rangle$ reduces to $\la defn -G |- e : T :: :: typing :: Ty_ by +G |- e : T :: :: Typing :: ty_ by ------------------ :: int G |- n : int diff --git a/src/grammar_pp.ml b/src/grammar_pp.ml index f192de4..cbaa3e1 100644 --- a/src/grammar_pp.ml +++ b/src/grammar_pp.ml @@ -2368,6 +2368,10 @@ and pp_element m xd sie in_type e = Some ("("^v^":"^t^")") | Coq co, Some (None,t) when co.coq_names_in_rules && (not in_type) -> Some ("(_:"^t^")") + | Lean co, Some (Some v,t) when (not in_type) -> + Some ("("^v^":"^t^")") + | Lean co, Some (None,t) when (not in_type) -> + Some ("(_:"^t^")") | Coq co, Some (v,t) when (not co.coq_names_in_rules) || in_type -> Some t | _, Some (v,t) -> From 5188ccb3d226a67dfccc910d11a4994ba58942de Mon Sep 17 00:00:00 2001 From: Peter Sewell Date: Sun, 15 Feb 2026 15:48:00 +0000 Subject: [PATCH 4/5] update l1.ott example for Lean generation (perhaps breaking it for other targets) --- examples/1Bsemantics/l1.ott | 6 +++--- revision_history.txt | 2 ++ 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/examples/1Bsemantics/l1.ott b/examples/1Bsemantics/l1.ott index 0de14a4..ba4553d 100644 --- a/examples/1Bsemantics/l1.ott +++ b/examples/1Bsemantics/l1.ott @@ -40,7 +40,7 @@ expr {{ lean Expr }}, e :: 'e_' ::= {{ com expressions }} | b :: :: bool | e1 op e2 :: :: op | if e1 then e2 else e3 :: :: if - | l := e :: :: assign + | l := e1 :: :: assign | ! l :: :: ref | skip :: :: skip | e1 ; e2 :: :: sequence @@ -52,11 +52,11 @@ v :: 'V_' ::= {{ com values }} | b :: :: bool | skip :: :: skip -store {{ lean Store }}, s :: 'store_' ::= {{ com stores }} {{ phantom }} {{ lem list (Location * integer) }} {{ coq list (Location * integer) }} {{ lean List (Location × Int) }} +store {{ lean Store }}, s :: 'store_' ::= {{ com stores }} {{ lem list (Location * integer) }} {{ coq list (Location * integer) }} {{ lean List (Location × Int) }} | empty :: :: empty {{ lem [] }} {{ coq [] }} {{ lean [] }} | s , l |-> n :: :: extend {{ lem (([[l]],[[n]])::[[s]]) }} {{ coq (([[l]],[[n]])::[[s]]) }} {{ lean (([[l]],[[n]])::[[s]]) }} -config {{ lean Config }}, c :: 'Config_' ::= {{ com configurations }} {{ phantom }} {{lem (expr*store) }} {{ coq (expr * store) }} {{ lean ([[Expr]] × [[Store]]) }} +config {{ lean Config }}, c :: 'Config_' ::= {{ com configurations }} {{lem (expr*store) }} {{ coq (expr * store) }} {{ lean ([[Expr]] × [[Store]]) }} | < e , s > :: :: config {{ lem ([[e]], [[s]]) }} {{ coq ([[e]], [[s]]) }} {{ lean ([[e]], [[s]]) }} typ {{ lean Typ }}, T :: 't_' ::= {{ com types }} diff --git a/revision_history.txt b/revision_history.txt index 9223f06..29e0af4 100644 --- a/revision_history.txt +++ b/revision_history.txt @@ -581,3 +581,5 @@ Peter Sewell + Thibaut Pérami: Add "menhir-start-type" hom to specify the top l 2024-12 @palmskog: only output plain comments in generated Coq code 2024-12-30 Version 0.34 + +2026-02-15 Peter Sewell: rudimentary Lean backend (generates well-typed Lean for examples/1Bsemantics/l1.ott; untested and probably broken for anything else) From dea15d60b2ec0f9c94f4385c9505b00dd989ce48 Mon Sep 17 00:00:00 2001 From: Peter Sewell Date: Tue, 10 Mar 2026 11:31:41 +0000 Subject: [PATCH 5/5] fix := bug in non-Lean output introduced with Lean commits --- src/grammar_pp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/grammar_pp.ml b/src/grammar_pp.ml index cbaa3e1..0632354 100644 --- a/src/grammar_pp.ml +++ b/src/grammar_pp.ml @@ -2692,7 +2692,7 @@ and pp_rule m xd r = (* returns a string option *) then None else Some - (strip_surrounding_parens (pp_nontermroot_ty m xd r.rule_ntr_name) ^ (match m with Lean _ -> " where" | _ -> " := ")^pp_com^"\n" + (strip_surrounding_parens (pp_nontermroot_ty m xd r.rule_ntr_name) ^ (match m with Lean _ -> " where" | _ -> " = ")^pp_com^"\n" ^ (match m with Lem _ -> " | " | _ -> " ") ^ String.concat (match m with Lean _ -> " " | _ -> " | ") (List.map