simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-05 19:00:33 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

wip: leancheck

Browse source
This commit is contained in:
Simon Cruanes 2023-04-20 22:05:15 -04:00
parent 8d70c10e18
commit 1530b761b0
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 13 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/leancheck/leancheck.ml
View file

@ -1,6 +1,7 @@
module T = Sidekick_cic_lib.Term
module Const = Sidekick_cic_lib.Const
module Level = Sidekick_cic_lib.Level
module Inductive = Sidekick_cic_lib.Inductive
let ( let@ ) = ( @@ )
@ -141,20 +142,24 @@ let process_files ~max_err (files : string list) : unit =
let ind ~n_params ~nidx ~tyidx ~intros ~univ_params : unit =
let name = Idx.get_name idx nidx in
let ty = Idx.get_term idx tyidx in
let intros =
let cstors =
List.map
(fun (i, j) -> Idx.get_name idx i, Idx.get_term idx j)
(fun (i, j) ->
{
Inductive.c_name = Idx.get_name idx i;
c_ty = Idx.get_term idx j;
})
intros
in
let univ_params =
List.map (fun i -> Idx.get_name idx i) univ_params
in
Fmt.eprintf "@[<2>>> @{<Green>Ind@} %s %a:%a [%d params] :=@ %a@]@."
name
Fmt.Dump.(list string)
univ_params T.pp_debug ty n_params
Fmt.(hvbox @@ Dump.(list @@ pair string T.pp_debug))
intros;
let spec = { Inductive.name; ty; n_params; univ_params; cstors } in
Fmt.eprintf "@[<2>@{<Green>Ind@}@ %a@]@." Inductive.pp_spec spec;
(* TODO: register to the conversion relation *)
Fmt.eprintf "is valid: %B@." (Inductive.is_valid spec);
()
let after_line () = Fmt.eprintf "%a@." Idx.dump idx