diff --git a/doc/invargent-manual.pdf b/doc/invargent-manual.pdf index 21c5fd9..d84de59 100644 Binary files a/doc/invargent-manual.pdf and b/doc/invargent-manual.pdf differ diff --git a/doc/invargent-manual.tm b/doc/invargent-manual.tm index e98d611..9d96fc0 100644 --- a/doc/invargent-manual.tm +++ b/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 , 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. @@ -543,10 +543,25 @@ <\auxiliary> <\collection> + <\associate|bib> + InvarGenT + <\associate|toc> - |math-font-series||1> + |math-font-series||1Introduction> |.>>>>|> + + |math-font-series||2Tutorial> + |.>>>>|> + + + |math-font-series||3Syntax> + |.>>>>|> + + + |math-font-series||4Solver + Parameters and CLI> |.>>>>|> + \ No newline at end of file diff --git a/src/Abduction.mli b/src/Abduction.mli index 400f5be..f57a1fc 100644 --- a/src/Abduction.mli +++ b/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 -> diff --git a/src/Infer.ml b/src/Infer.ml index c55031e..d4524ad 100644 --- a/src/Infer.ml +++ b/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 diff --git a/src/Infer.mli b/src/Infer.mli index 76b2d15..97fda27 100644 --- a/src/Infer.mli +++ b/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. *) diff --git a/src/InvarGenT.ml b/src/InvarGenT.ml index e98ae50..83a89e6 100644 --- a/src/InvarGenT.ml +++ b/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,6 +61,60 @@ 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 @@ -73,15 +122,4 @@ let () = 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 () diff --git a/src/NumS.mli b/src/NumS.mli index 2f44f5f..404cbb5 100644 --- a/src/NumS.mli +++ b/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. *) diff --git a/src/OCaml.ml b/src/OCaml.ml index 882cf1d..dc797bf 100644 --- a/src/OCaml.ml +++ b/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" diff --git a/src/OCaml.mli b/src/OCaml.mli index b7a8b3a..5e821e7 100644 --- a/src/OCaml.mli +++ b/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