@@ -11,6 +11,7 @@ let ast_flag = ref false
1111let result_flag = ref false
1212let no_run_flag = ref false
1313let run_f_flag = ref false
14+ let no_sig_flag = ref false
1415
1516let trace_phase name = if ! trace_flag then print_endline (" -- " ^ name)
1617
@@ -64,20 +65,21 @@ let state = ref Lambda.Env.empty
6465let f_state = ref []
6566
6667let print_sig s =
67- match s with
68- | Types. ExT (aks , Types. StrT(tr )) ->
69- List. iter (fun (a , k ) ->
70- Format. open_box 0 ;
71- Format. print_string (" ? " ^ a ^ " : " );
72- Types. print_kind k;
73- Format. print_break 1 0 ;
74- Format. close_box ()
75- ) aks;
76- Types. print_row tr;
77- print_endline " "
78- | _ ->
79- Types. print_extyp s;
80- print_endline " "
68+ if not ! no_sig_flag then
69+ match s with
70+ | Types. ExT (aks , Types. StrT(tr )) ->
71+ List. iter (fun (a , k ) ->
72+ Format. open_box 0 ;
73+ Format. print_string (" ? " ^ a ^ " : " );
74+ Types. print_kind k;
75+ Format. print_break 1 0 ;
76+ Format. close_box ()
77+ ) aks;
78+ Types. print_row tr;
79+ print_endline " "
80+ | _ ->
81+ Types. print_extyp s;
82+ print_endline " "
8183
8284let rec unpack = function
8385 | Fomega. PackE (_ , v , _ ) -> unpack v
@@ -218,6 +220,7 @@ let argspec = Arg.align
218220 " -c" , Arg. Set Elab. verify_flag, " check target program" ;
219221 " -d" , Arg. Set no_run_flag, " dry, do not run program" ;
220222 " -f" , Arg. Set run_f_flag, " run program as System F reduction" ;
223+ " -no-sig" , Arg. Set no_sig_flag, " do not print signature" ;
221224 " -p" , Arg. Set ast_flag, " show parse tree" ;
222225 " -r" , Arg. Set result_flag, " show resulting term" ;
223226 " -t" , Arg. Set trace_flag, " trace compiler phases" ;
0 commit comments