The Command Line Interface.

doc/invargent-manual.tm

@@ -37,12 +37,12 @@
   local type variables for the hidden parts of the type encapsulated in a
   GADT.
 
-  Our type system for GADTs differs from more pragmatic approaches in
-  mainstream functional languages in that we do not require any type
-  annotations on expressions, even on recursive functions. Our
-  implementation: InvarGenT, see <cite|InvarGenT>, also includes linear
-  equations and inequalities over rational numbers in the language of types,
-  with the possibility to introduce more domains in the future.
+  The InvarGenT type system for GADTs differs from more pragmatic approaches
+  in mainstream functional languages in that we do not require any type
+  annotations on expressions, even on recursive functions. The implementation
+  also includes linear equations and inequalities over rational numbers in
+  the language of types, with the possibility to introduce more domains in
+  the future.
 
   <section|Tutorial>
 
@@ -543,10 +543,25 @@
 
 <\auxiliary>
   <\collection>
+    <\associate|bib>
+      InvarGenT
+    </associate>
     <\associate|toc>
-      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|1<space|2spc>>
+      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|1<space|2spc>Introduction>
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
       <no-break><pageref|auto-1><vspace|0.5fn>
+
+      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|2<space|2spc>Tutorial>
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-2><vspace|0.5fn>
+
+      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|3<space|2spc>Syntax>
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-3><vspace|0.5fn>
+
+      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|4<space|2spc>Solver
+      Parameters and CLI> <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-4><vspace|0.5fn>
     </associate>
   </collection>
 </auxiliary>

src/Abduction.mli

@@ -12,6 +12,9 @@ val skip_kind : skip_kind ref
     try [more_general=true] (gives the same or better answers). *)
 val more_general : bool ref
 
+val timeout_count : int ref
+val fail_timeout_count : int ref
+val no_alien_prem : bool ref
 
 val abd_simple :
   Terms.quant_ops ->

src/Infer.ml

@@ -8,6 +8,7 @@
 
 let annotating_fun = ref true
 let annotating_letin = ref false
+let inform_toplevel = ref false
 
 open Terms
 open Aux
@@ -820,6 +821,9 @@ let infer_prog solver prog =
           gamma := (x, typ_sch) :: !gamma;
           let ex_items =
             update_new_ex_types q new_ex_types sb_res sb_chi in
+          if !inform_toplevel
+          then Format.printf
+              "@[<2>val@ %s :@ %a@]@\n%!" x pr_typscheme typ_sch;
           ex_items @ [ILetRecVal (x, e, typ_sch, tests, elim_extypes, loc)]
         | new_ex_types, LetVal (p, e, defsig, tests, loc) ->
           let avs, sig_vs, sig_cn, t = match defsig with
@@ -888,7 +892,11 @@ let infer_prog solver prog =
                 "LetVal: x=%s@ res=%a@ nice res=%a@ gvs=%a@ phi=%a@\n%!"
                 x pr_ty res pr_ty res'
                 pr_vars gvs pr_formula phi; *]*)
-              x, (VarSet.elements gvs, phi, res')
+              let typ_sch = VarSet.elements gvs, phi, res' in
+              if !inform_toplevel
+              then Format.printf
+                  "@[<2>val@ %s :@ %a@]@\n%!" x pr_typscheme typ_sch;
+              x, typ_sch
             else fun (x, res) ->
               let res = subst_typ exsb res in
               let gvs, phi = prepare_scheme phi res in
@@ -921,7 +929,12 @@ let infer_prog solver prog =
               *]*)
               (* Here in [ety] the variables are free, unlike the
                  occurrences in [exphi]. *)
-              x, (gvs, phi, TCons (ety_n, List.map (fun v->TVar v) pvs)) in
+              let typ_sch =
+                gvs, phi, TCons (ety_n, List.map (fun v->TVar v) pvs) in
+              if !inform_toplevel
+              then Format.printf
+                  "@[<2>val@ %s :@ %a@]@\n%!" x pr_typscheme typ_sch;  
+              x, typ_sch in
           let typ_schs = List.map typ_sch_ex env in
           gamma := typ_schs @ !gamma;
           ex_items @ List.rev !more_items

src/Infer.mli

@@ -8,6 +8,7 @@
 
 val annotating_fun : bool ref
 val annotating_letin : bool ref
+val inform_toplevel : bool ref
 
 (** Each disjunct stores a trigger to be called when other disjuncts
     are eliminated during normalization-simplification. *)

src/InvarGenT.ml

@@ -18,7 +18,7 @@ let solver ~new_ex_types ~preserve cn =
   let brs = Infer.simplify preserve q_ops brs in
   Invariants.solve q_ops new_ex_types exty_res_of_chi brs
 
-let process_file ?(do_sig=false) ?(do_ml=false) ?(do_mli=false)
+let process_file ?(do_sig=false) ?(do_ml=false)
     ?(verif_ml=true) ?(full_annot=false) fname =
   current_file_name := fname;
   let infer_annot_fun = !Infer.annotating_fun in
@@ -43,11 +43,6 @@ let process_file ?(do_sig=false) ?(do_ml=false) ?(do_mli=false)
     Format.fprintf output "%a@\n%!"
       (OCaml.pr_ml ~funtys:full_annot ~lettys:full_annot) annot;
     Format.printf "InvarGenT: Generated file %s@\n%!" (base^".ml"));
-  if do_mli then (
-    let output = Format.formatter_of_out_channel
-        (open_out (base^".mli")) in
-    Format.fprintf output "%a@\n%!" OCaml.pr_mli annot;
-    Format.printf "InvarGenT: Generated file %s@\n%!" (base^".mli"));
   if do_ml && verif_ml then
     let cmd = "ocamlc -c "^base^".ml" in
     let res = Sys.command cmd in
@@ -66,22 +61,65 @@ let process_file ?(do_sig=false) ?(do_ml=false) ?(do_mli=false)
       Some res)
   else None
 
+let main () =
+  let do_ml = ref true
+  and do_sig = ref true
+  and verif_ml = ref true
+  and full_annot = ref false in
+  let cli = [
+    "-inform", Arg.Set Infer.inform_toplevel,
+    "Print type schemes of toplevel definitions as they are inferred";
+    "-no_sig", Arg.Clear do_sig,
+    "Do not generate the `.gadti` file";
+    "-no_ml", Arg.Clear do_ml,
+    "Do not generate the `.ml` file";
+    "-no_verif", Arg.Clear verif_ml,
+    "Do not call `ocamlc -c` on the generated `.ml` file";
+    "-full_annot", Arg.Set full_annot,
+    "Annotate the `function` and `let..in` nodes in generated OCaml code";
+    "-term_abduction_timeout", Arg.Set_int Abduction.timeout_count,
+    "Limit on term simple abduction steps (default 700)";
+    "-term_abduction_fail", Arg.Set_int Abduction.fail_timeout_count,
+    "Limit on backtracking steps in term joint abduction (default 4)";
+    "-no_alien_prem", Arg.Set Abduction.no_alien_prem,
+    "Do not include alien (e.g. numerical) premise info in term abduction";
+    "-early_num_abduction", Arg.Set NumS.early_num_abduction,
+    "Include recursive branches in numerical abduction from the start";
+    "-num_abduction_rotations", Arg.Set_int NumS.abd_rotations,
+    "Numerical abduction: coefficients from +/- 1/N to +/- N (default 3)";
+    "-num_prune_at", Arg.Set_int NumS.abd_prune_at,
+    "Keep less than N elements in abduction sums (default <6)";
+    "-num_abduction_timeout", Arg.Set_int NumS.abd_timeout_count,
+    "Limit on numerical simple abduction steps (default 1000)";
+    "-num_abduction_fail", Arg.Set_int NumS.abd_fail_timeout_count,
+    "Limit on backtracking steps in numerical joint abduction (default 10)";
+    "-disjelim_rotations", Arg.Set_int NumS.disjelim_rotations,
+    "Disjunction elimination: check coefficients from 1/N (default 3)";
+    "-passing_ineq_trs", Arg.Set NumS.passing_ineq_trs,
+    "Include inequalities in conclusion when solving numerical abduction";
+    "-not_annotating_fun", Arg.Clear Infer.annotating_fun,
+    "Do not keep information for annotating `function` nodes";
+    "-annotating_letin", Arg.Set Infer.annotating_letin,
+    "Keep information for annotating `function` nodes";
+    "-let_in_fallback", Arg.Set let_in_fallback,
+    "Annotate `let..in` nodes in fallback mode of .ml generation";
+  ] in
+  let fname = ref "" in
+  let anon_fun f = fname := f in
+  let msg = "Usage: "^Sys.argv.(0)^"[OPTIONS] source_file.gadt" in
+  Arg.parse cli anon_fun msg;
+  try
+    ignore
+      (process_file !fname ~do_sig:!do_sig ~do_ml:!do_ml
+         ~verif_ml:!verif_ml ~full_annot:!full_annot)
+  with (Report_toplevel _ | Contradiction _) as exn ->
+    pr_exception Format.std_formatter exn; exit 2
+
 
 let () =
   let executable = Filename.basename Sys.executable_name in
   let chop f =
     try Filename.chop_extension f with Invalid_argument _ -> f in
   let executable = chop (chop executable) in
   if executable <> "Tests" && executable <> "InvarGenTTest"
-  then (
-    if Array.length Sys.argv <= 1 then (
-      print_string ("Usage: "^Sys.argv.(0)^" \"program source file\"\n");
-      exit 0
-    ) else (
-      let file_name = Sys.argv.(1) in
-      try
-        ignore
-          (process_file file_name ~do_sig:true ~do_ml:true ~do_mli:true)
-      with (Report_toplevel _ | Contradiction _) as exn ->
-        pr_exception Format.std_formatter exn; exit 2)
-  )
+  then main ()

src/NumS.mli

@@ -10,6 +10,11 @@
 val abd_rotations : int ref
 (** Start abduction on all branches rather than only non-recursive. *)
 val early_num_abduction : bool ref
+(** Keep less than N elements in abduction sums (default <6). *)
+val abd_prune_at : int ref
+val abd_timeout_count : int ref
+val abd_fail_timeout_count : int ref
+val passing_ineq_trs : bool ref
 (** For uniformity, return an empty list as introduced
     variables. Raise [Contradiction] if constraints are contradictory
     and [Suspect] if no answer can be found. *)

src/OCaml.ml

@@ -317,5 +317,3 @@ let pr_ml ~funtys ~lettys ppf prog =
                          (cns_str n) (List.length cs))) constrs; *]*)
   fprintf ppf "type num = int@\n";
   pr_struct_items ~funtys ~lettys constrs ppf init_types CNames.empty prog
-
-let pr_mli ppf prog = failwith "not implemented yet"

src/OCaml.mli

@@ -9,5 +9,3 @@
 val pr_ml :
   funtys:bool -> lettys:bool ->
   Format.formatter -> Terms.annot_item list -> unit
-
-val pr_mli : Format.formatter -> Terms.annot_item list -> unit