Formatter updates, allow spec to be read from cli

.gitignore

@@ -10,6 +10,9 @@ _coverage
 # vscode settings
 .vscode
 
+# Mac OS
+.DS_Store
+
 # Executable
 adelfa
 

.ocamlformat

@@ -1,2 +1,5 @@
 profile = janestreet
 version = 0.26.1
+
+wrap-comments=true
+assignment-operator=end-line

Makefile

@@ -17,8 +17,8 @@ debug:
 install: main
 	@dune install
 
-.PHONY: tar
-tar :
+.PHONY: bundle
+bundle :
 	@dune exec ./bundle/bundle.exe
 
 .PHONY: test

bin/main.ml

@@ -19,7 +19,6 @@ let interactive = ref true
 let out = ref stdout
 let switch_to_interactive = ref false
 let lexbuf = ref (Lexing.from_channel stdin)
-let count = State.rref 0
 let inputFile = ref None
 
 let perform_switch_to_interactive () =
@@ -35,13 +34,13 @@ let interactive_or_exit () =
   then if !switch_to_interactive then perform_switch_to_interactive () else exit 1
 ;;
 
-(* if interactive, reset line count to provide
-   more accurate error position information. *)
+(* if interactive, reset line count to provide more accurate error position
+   information. *)
 let reset_if_interactive () =
   if !interactive
   then
-    !lexbuf.lex_curr_p
-    <- { !lexbuf.lex_curr_p with pos_cnum = 0; pos_bol = 0; pos_lnum = 1 }
+    !lexbuf.lex_curr_p <-
+      { !lexbuf.lex_curr_p with pos_cnum = 0; pos_bol = 0; pos_lnum = 1 }
 ;;
 
 let position_range (p1, p2) =
@@ -72,22 +71,49 @@ let setInputFile name =
   | Some _ -> failwith "Error: More than one input file specified."
 ;;
 
+let read_spec filename =
+  if Prover.has_sig ()
+  then failwithf "Specification file already given. Not reading `%s'" filename;
+  let inchan = open_in filename in
+  let lexbuf = Lexing.from_channel inchan in
+  try
+    while true do
+      let udecl = TwelfParser.decl TwelfLexer.token lexbuf in
+      match udecl with
+      | Uterms.Const (id, utm) ->
+        let tm, _ = Translate.trans_term !Prover.lf_sig [] [] [] [] (Some Type.oty) utm in
+        if Term.is_kind tm
+        then (
+          let tydecl = Signature.ty_dec id tm 0 Signature.NoFixity [] in
+          Prover.set_sig (Signature.add_type_decl !Prover.lf_sig tydecl))
+        else (
+          let odecl = Signature.obj_dec id tm 0 Signature.NoFixity in
+          Prover.set_sig (Signature.add_obj_decl !Prover.lf_sig odecl))
+      | Fixity _ -> bugf "Expected const reading specification"
+    done
+  with
+  | End_of_file ->
+    close_in inchan;
+    ()
+;;
+
 let checkInput () =
   match !inputFile with
   | None -> ()
   | Some fname ->
     if Sys.file_exists fname
     then (
       lexbuf := Lexing.from_channel (open_in fname);
-      !lexbuf.Lexing.lex_curr_p
-      <- { !lexbuf.Lexing.lex_curr_p with Lexing.pos_fname = fname })
+      !lexbuf.Lexing.lex_curr_p <-
+        { !lexbuf.Lexing.lex_curr_p with Lexing.pos_fname = fname })
     else failwithf "Error: Invalid input file: `%s'." fname
 ;;
 
 let usageMsg = "Usage: adelfa [options]\noptions are: "
 
 let specList =
   [ "-i", Arg.String setInputFile, " Specifies a file from which to read input."
+  ; "-s", Arg.String read_spec, " Specified a file from which to read a specification."
   ; "--input", Arg.String setInputFile, " Specifies a file from which to read input."
   ; "-a", Arg.Set Globals.annotate, " Annotate mode"
   ]
@@ -106,55 +132,23 @@ let print_proof_prompt () =
   flush stdout
 ;;
 
-let read_spec filename =
-  if Prover.has_sig ()
-  then failwithf "Specification file already given. Not reading `%s'" filename;
-  let inchan = open_in filename in
-  let lexbuf = Lexing.from_channel inchan in
-  try
-    while true do
-      let udecl = TwelfParser.decl TwelfLexer.token lexbuf in
-      match udecl with
-      | Uterms.Const (id, utm) ->
-        let tm, _ = Translate.trans_term !Prover.lf_sig [] [] [] [] (Some Type.oty) utm in
-        if Term.is_kind tm
-        then (
-          let tydecl = Signature.ty_dec id tm 0 Signature.NoFixity [] in
-          Prover.set_sig (Signature.add_type_decl !Prover.lf_sig tydecl))
-        else (
-          let odecl = Signature.obj_dec id tm 0 Signature.NoFixity in
-          Prover.set_sig (Signature.add_obj_decl !Prover.lf_sig odecl))
-      | Fixity _ -> bugf "Expected const reading specification"
-    done
-  with
-  | End_of_file ->
-    close_in inchan;
-    ()
-;;
-
 let handle_common v =
   match v with
   | Uterms.Undo -> State.Undo.back 2
   | Uterms.Set s -> Prover.change_settings s
 ;;
 
-(* process proof tactics for deriving the current theorem.
-   Read from a file or stdin *)
+(* process proof tactics for deriving the current theorem. Read from a file or stdin *)
 let process_proof () =
-  (* read in tactic, call appropriate step in prover.
-     if proof complete is raised return to outer loop. *)
+  (* read in tactic, call appropriate step in prover. if proof complete is raised return
+     to outer loop. *)
   if !Globals.annotate
   then (
     fprintf !out "</pre>\n%!";
-    incr count;
-    fprintf !out "<a name=\"%d\"></a>\n%!" !count;
     fprintf !out "<pre>\n%!");
   print_proof_prompt ();
   let input = Parser.command Lexer.token !lexbuf in
-  if not !interactive
-  then (
-    let pre, post = if !Globals.annotate then "<b>", "</b>" else "", "" in
-    fprintf !out "%s%s%s\n%!" pre (Print.string_of_command input) post);
+  if not !interactive then fprintf !out "%s\n%!" (Print.string_of_command input);
   match input with
   | Uterms.Abort -> raise End_of_file
   | Uterms.Skip -> Prover.skip ()
@@ -175,8 +169,8 @@ let process_proof () =
   | Uterms.Case (Uterms.Keep hyp) -> Prover.case false hyp
   | Uterms.Case (Uterms.Remove hyp) -> Prover.case true hyp
   | Uterms.Exists utm ->
-    (* weak type checking/inference must be done on utm using current proof state
-       then call Prover.exsits*)
+    (* weak type checking/inference must be done on utm using current proof state then
+       call Prover.exsits*)
     let nvars =
       List.filter
         (fun (_, t) -> Term.is_var Term.Nominal t)
@@ -223,8 +217,8 @@ let process_proof () =
         nvar_ctx
         uform
     in
-    (* Find new variable occurrences and add them to the sequent - replacing
-       them with nominals *)
+    (* Find new variable occurrences and add them to the sequent - replacing them with
+       nominals *)
     Prover.assert_thm depth form
   | Uterms.Weaken (clear, utm, depth) ->
     let nvars =
@@ -286,23 +280,15 @@ let process_proof () =
   | Uterms.Common v -> handle_common v
 ;;
 
-(* Process toplevel commands;
-   either from file or interactive *)
+(* Process toplevel commands; either from file or interactive *)
 let process_top_level () =
   (* parse top-level command from stdin, or file *)
   (* if no LF signature loaded, error on any other commands *)
   (* if a theorem is stated, enter proof construction *)
-  if !Globals.annotate
-  then (
-    incr count;
-    fprintf !out "<a name=\"%d\"></a>\n%!" !count;
-    fprintf !out "<pre class=\"code\">\n%!");
+  if !Globals.annotate then fprintf !out "<pre>\n%!";
   print_top_prompt ();
   let input = Parser.top_command Lexer.token !lexbuf in
-  if not !interactive
-  then (
-    let pre, post = if !Globals.annotate then "<b>", "</b>" else "", "" in
-    fprintf !out "%s%s%s\n%!" pre (Print.string_of_topcommand input) post);
+  if not !interactive then fprintf !out "%s\n%!" (Print.string_of_topcommand input);
   (match input with
    | Uterms.Theorem (name, uthm) ->
      proof_steps := 0;

examples/lambda-calc/subject_reduction/stlc.ath

@@ -0,0 +1,18 @@
+Specification "stlc.lf".
+
+%subject reduction for stlc
+Theorem sr_eval : forall E V T D1 D2,
+                    {D1 : eval E V} => {D2 : of E T} => exists D, {D : of V T}.
+induction on 1. intros. case H1.
+  %case 1: application; D1 = eval-app M N V R T1 a1 a2, E = app M N
+    case H2. %D2 = of_app M N T D3 D4 D5
+    apply IH to H8 H14.
+    case H16.
+    inst H20 with n2 = N. inst H21 with n3 = D5.
+    apply IH to H9 H22.
+    exists (D n3 n2 n1 n).
+    search.
+  %case 2: abstraction; D1 = eval-abs R T1, E = abs T1 ([x]R x)
+    exists D2.
+    search.
+

examples/lambda-calc/subject_reduction/stlc.lf

@@ -0,0 +1,21 @@
+ty : type.
+arr : {T:ty}{U:ty} ty.
+
+tm : type.
+app : {E1:tm}{E2:tm} tm.
+abs : {T:ty}{R:{x:tm}tm} tm.
+
+of : {E:tm}{T:ty}type.
+of_app : {M:tm}{N:tm}{T:ty}{U:ty}
+           {a1:of M (arr U T)} {a2:of N U}
+           of (app M N) T.
+of_abs : {R : {x:tm} tm}{T:ty}{U:ty}
+           {a1:({x:tm}{z:of x T} of (R x) U)}
+           of (abs T ([x] R x)) (arr T U).
+
+eval : {E1:tm}{E2:tm}type.
+eval_abs : {R: {x:tm} tm}{T:ty}
+             eval (abs T ([x] R x)) (abs T ([x] R x)).
+eval_app : {M:tm}{N:tm}{V:tm}{R:{x:tm} tm}{T:ty}
+             {a1:eval M (abs T ([x] R x))}{a2:eval (R N) V}
+             eval (app M N) V.

examples/orbi/equal-untyped/equal-untyped.lf

@@ -1,5 +1,5 @@
 tm: type.
-lam: {M: {x:tm} tm} tm.
+lam: {M: tm -> tm} tm.
 app: {M1:tm}{M2:tm} tm.
 
 aeq: tm -> tm -> type.
@@ -8,21 +8,21 @@ deq: tm -> tm -> type.
 ae_a : {M1: tm}{M2: tm}{N1:tm}{N2:tm}
        {D1:aeq M1 N1}{D2:aeq M2 N2}
        aeq (app M1 M2) (app N1 N2).
-ae_l : {M:{x:tm} tm}{N:{y:tm} tm}
-       {D: {z:tm}{D1: aeq z z} aeq (M z) (N z)}
+ae_l : {M: tm -> tm}{N: tm -> tm}
+       {D: {z:tm} aeq z z -> aeq (M z) (N z)}
        aeq (lam ([x] M x)) (lam ([x] N x)).
 
 de_a : {M1:tm}{M2:tm}{N1:tm}{N2:tm}
        {D1: deq M1 N1}{D2: deq M2 N2}
        deq (app M1 M2) (app N1 N2).
-de_l : {M: {x:tm} tm}{N: {x:tm} tm}
-       {D: {z:tm}{D1:deq z z} deq (M z) (N z)}
+de_l : {M: tm -> tm}{N: tm -> tm}
+       {D: {z:tm} deq z z -> deq (M z) (N z)}
        deq (lam ([x] M x)) (lam ([x] N x)).
-de_r : {M:tm} deq M M.
 de_s : {M:tm}{N:tm}
        {D: deq M N}
        deq N M.
 de_t : {M1:tm}{M2:tm}{M3:tm}
        {D1: deq M1 M2}
        {D2: deq M2 M3}
        deq M1 M3.
+de_r : {M:tm} deq M M.

examples/prog-lang/poplmark/1a.ath

@@ -13,18 +13,6 @@ Schema wf :=
 Theorem sub__ty : ctx L:c, forall D U1 U2, {L |- D : sub U1 U2} => {L |- U1 : ty} /\ {L |- U2 : ty}.
 intros. split. search. search.
 
-%Derivations for types "ty" and "var" cannot depend on assumptions of type
-%"bound" or "bound_var". We show this by inducion on the assumption
-%derivation of type ty or type var, showing that in each case the term
-%could not exhibit a dependency on such assumptions.
-%
-%These results will be used in proving a narrowing result for the types "ty"
-%and "var" which is useful in showing narrowing of subtyping judgments.
-
-%With the strengthening results above, narrowing for these types is proved
-%directly by strengthening the assumption derivation and then weakening it
-%with the desired context items.
-
 Theorem narrow_ty : ctx L:c, forall Q X P D T: o -> o -> o DV,
   {L |- X : ty} => {L |- DV : var X} =>
   {L |- D : sub P Q} =>
@@ -282,20 +270,20 @@ Theorem subty-refl : ctx L:c, forall Q D,
 induction on 1.
 intros. case H1 (keep).
 case H2.
-apply IH to H3 H7.
-weaken H4 with var n.
-weaken H3 with ty.
-weaken H11 with var n4.
-weaken H10 with bound n T. weaken H12 with bound n4 T.
-weaken H13 with bound_var n T n6 n3. weaken H14 with bound_var n4 T n7 n5.
-weaken H8 with var n2.
-weaken H17 with bound n2 T.
-weaken H18 with bound_var n2 T n11 n10.
-apply IH to H15 H19 with (L = L, n3:ty, n2:var n3, n1:bound n3 T, n:bound_var n3 T n1 n2).
-prune H20.
-exists sa-all T F T F (D' n2 n1 n) (D'1). search.
-case H2.
-apply IH to H3 H7. apply IH to H4 H8. exists sa-arrow T1 T2 T1 T2 D' D'1. search.
-exists sa-top top. search.
-case H2.
-case H2.
+  apply IH to H3 H7.
+  weaken H4 with var n.
+  weaken H3 with ty.
+  weaken H11 with var n4.
+  weaken H10 with bound n T. weaken H12 with bound n4 T.
+  weaken H13 with bound_var n T n6 n3. weaken H14 with bound_var n4 T n7 n5.
+  weaken H8 with var n2.
+  weaken H17 with bound n2 T.
+  weaken H18 with bound_var n2 T n11 n10.
+  apply IH to H15 H19 with (L = L, n3:ty, n2:var n3, n1:bound n3 T, n:bound_var n3 T n1 n2).
+  prune H20.
+  exists sa-all T F T F (D' n2 n1 n) (D'1). search.
+  case H2.
+  apply IH to H3 H7. apply IH to H4 H8. exists sa-arrow T1 T2 T1 T2 D' D'1. search.
+  exists sa-top top. search.
+  case H2.
+  case H2.

examples/prog-lang/poplmark/1a.lf

@@ -32,22 +32,3 @@ wfty-arrow : {T1:ty}{T2:ty}
 wfty-all : {T1:ty}{T2:{x:ty} ty}
             {d1: wfty T1 }{d2: ({x:ty} wfty (T2 x))}
              wfty (all T1 ([x] T2 x)).
-
-
-% Some equality definitions for use in strengthening lemmas
-eq_ty : {X:ty}{S:ty}{DV:var X}
-        {T1:{x:bound X S}{y:bound_var X S x DV}ty}
-        {T2:{x:bound X S}{y:bound_var X S x DV}ty}
-        type.
-refl_ty : {X:ty}{S:ty}{DV:var X}
-          {T:{x:bound X S}{y:bound_var X S x DV}ty}
-          eq_ty X S DV T T.
-
-eq_var : {Q:ty}{X:ty}{S:ty}{DV:var X}
-         {T1:{x:bound X S}{y:bound_var X S x DV}var Q}
-         {T2:{x:bound X S}{y:bound_var X S x DV}var Q}
-         type.
-
-refl_var : {Q:ty}{X:ty}{S:ty}{DV:var X}
-           {T:{x:bound X S}{y:bound_var X S x DV}var Q}
-           eq_var Q X S DV T T.

src/context.ml

@@ -402,10 +402,9 @@ let block_eq_sub sub_rel a b1 b2 =
     |> Option.is_some
 ;;
 
-(* splits a context by the location of n.
-   n is assumed to appear in the explicit part of g.
-   returns the context to the left of n, the type of n, and the
-   context to the right of n. *)
+(* splits a context by the location of n. n is assumed to appear in the explicit part of
+   g. returns the context to the left of n, the type of n, and the context to the right of
+   n. *)
 let split_ctx g n =
   let rec find g g2 =
     match g with