Skip to content

Commit

Permalink
code formatting
Browse files Browse the repository at this point in the history
  • Loading branch information
@tsani
tsani committed Sep 19, 2018
1 parent fccb33c commit 66c66c4
Show file tree
Hide file tree
Showing 2 changed files with 67 additions and 75 deletions.
38 changes: 15 additions & 23 deletions src/core/command.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,21 +12,6 @@ type command =

(* The built in commands *)

(* args = (i, e, []) where
i : hole number
e : name of a variable appearing in the ith hole
let split = {name = "split";
run = (fun ppf args ->
let i = args.hd in
let e = args.tl.hd in
let (loc, cD,cG,(tau,theta)) = Holes.getHole i in
try
Interactive.split e cD cG
with _ -> "?"
);
help = " ... " }
*)

(** Used to define command bodies requiring a certain number of arguments.
* This function checks the length of the argument list against the
* given number, and in case of success runs the given command body
Expand Down Expand Up @@ -416,15 +401,22 @@ let printfun =
command_with_arguments 1
(fun ppf [arg] ->
try
let (cidlist,_) = List.split (List.fold_left (fun acc l -> acc@(!l)) [] (DynArray.to_list Comp.entry_list)) in
let (cidlist, _) =
List.split
(List.fold_left
(fun acc l -> acc@(!l))
[]
(DynArray.to_list Comp.entry_list))
in
let entrylist = List.rev_map Comp.get cidlist in
let entry = List.find (fun x -> arg = (Id.string_of_name x.Comp.name)) entrylist in
(match entry.Comp.prog with
| Synint.Comp.RecValue (prog, ec, _ms, _env) ->
ppr_sgn_decl (Synint.Sgn.Rec[(prog,entry.Comp.typ ,ec)]);
fprintf ppf ";\n"
| _ -> fprintf ppf "- %s is not a function.;\n" arg
)
let entry =
List.find
(fun x -> arg = (Id.string_of_name x.Comp.name)) entrylist
in
match entry.Comp.prog with
| Synint.Comp.RecValue (prog, ec, _ms, _env) ->
ppr_sgn_decl (Synint.Sgn.Rec[(prog,entry.Comp.typ ,ec)])
| _ -> fprintf ppf "- %s is not a function.;\n" arg
with
| Not_found ->
fprintf ppf "- The function %s does not exist;\n" arg
Expand Down
104 changes: 52 additions & 52 deletions src/core/pretty.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1437,60 +1437,60 @@ module Int = struct


| Comp.Branch (_, cD1', _cG, Comp.PatMetaObj (_, mO), t, e) ->
if !Control.printNormal then
(match e with
| Comp.Hole (loc, name) ->
fprintf ppf "\n@[<v2>| %a => %a@]"
(fmt_ppr_meta_obj cD1' 0) mO
(fmt_ppr_cmp_exp_chk cD1' cG 1) e
| _ ->
fprintf ppf "@ @[<v2>| @[<v0>%a@[%a@ => @]@ @[<2>@ %a@]@] @]@ "
(fmt_ppr_cmp_branch_prefix 0) cD1'
(fmt_ppr_meta_obj cD1' 0) mO
(* NOTE: Technically: cD |- cG ctx and
* cD1' |- mcomp (MShift n) t <= cD where n = |cD1|
* -bp
*)
(fmt_ppr_cmp_exp_chk cD1' cG 1) e)
else
fprintf ppf "@ @[<v2>| @[<v0>%a@[%a : %a @] => @]@ @[<2>@ %a@]@]@ "
(fmt_ppr_cmp_branch_prefix 0) cD1'
(fmt_ppr_meta_obj cD1' 0) mO
(* this point is where the " : " is in the string above *)
(fmt_ppr_refinement cD1' cD 2) t
(* NOTE: Technically: cD |- cG ctx and
* cD1' |- mcomp (MShift n) t <= cD where n = |cD1|
* -bp
*)
(fmt_ppr_cmp_exp_chk cD1' cG 1) e
if !Control.printNormal then
(match e with
| Comp.Hole (loc, name) ->
fprintf ppf "\n@[<v2>| %a => %a@]"
(fmt_ppr_meta_obj cD1' 0) mO
(fmt_ppr_cmp_exp_chk cD1' cG 1) e
| _ ->
fprintf ppf "@ @[<v2>| @[<v0>%a@[%a@ => @]@ @[<2>@ %a@]@] @]@ "
(fmt_ppr_cmp_branch_prefix 0) cD1'
(fmt_ppr_meta_obj cD1' 0) mO
(* NOTE: Technically: cD |- cG ctx and
* cD1' |- mcomp (MShift n) t <= cD where n = |cD1|
* -bp
*)
(fmt_ppr_cmp_exp_chk cD1' cG 1) e)
else
fprintf ppf "@ @[<v2>| @[<v0>%a@[%a : %a @] => @]@ @[<2>@ %a@]@]@ "
(fmt_ppr_cmp_branch_prefix 0) cD1'
(fmt_ppr_meta_obj cD1' 0) mO
(* this point is where the " : " is in the string above *)
(fmt_ppr_refinement cD1' cD 2) t
(* NOTE: Technically: cD |- cG ctx and
* cD1' |- mcomp (MShift n) t <= cD where n = |cD1|
* -bp
*)
(fmt_ppr_cmp_exp_chk cD1' cG 1) e

| Comp.Branch (_, cD1', cG', pat, t, e) ->
let cG_t = cG (* Whnf.cnormCtx (cG, t) *) in
let cG_ext = Context.append cG_t cG' in

if !Control.printNormal then
(* fprintf ppf "@ @[<v2>| @[<v0>%a ; %a@[ |- %a @] => @]@ @[<2>@ %a@]@]@ "
(fmt_ppr_cmp_branch_prefix 0) cD1'
(fmt_ppr_cmp_gctx cD1' 0) cG' *)
fprintf ppf "@ @[| %a => %a@]@ "
(fmt_ppr_pat_obj cD1' cG' 0) pat
(* NOTE: Technically: cD |- cG ctx and
* cD1' |- mcomp (MShift n) t <= cD where n = |cD1|
* -bp
*)
(fmt_ppr_cmp_exp_chk cD1' cG_ext 1) e
else
fprintf ppf "@ @[<v2>| @[<v0>%a ; %a@[ |- %a : %a @] => @]@ @[<2>@ %a@]@]@ "
(fmt_ppr_cmp_branch_prefix 0) cD1'
(fmt_ppr_cmp_gctx cD1' 0) cG'
(fmt_ppr_pat_obj cD1' cG' 0) pat
(* this point is where the " : " is in the string above *)
(fmt_ppr_refinement cD1' cD 2) t
(* NOTE: Technically: cD |- cG ctx and
* cD1' |- mcomp (MShift n) t <= cD where n = |cD1|
* -bp
*)
(fmt_ppr_cmp_exp_chk cD1' cG_ext 1) e
let cG_t = cG (* Whnf.cnormCtx (cG, t) *) in
let cG_ext = Context.append cG_t cG' in

if !Control.printNormal then
(* fprintf ppf "@ @[<v2>| @[<v0>%a ; %a@[ |- %a @] => @]@ @[<2>@ %a@]@]@ "
(fmt_ppr_cmp_branch_prefix 0) cD1'
(fmt_ppr_cmp_gctx cD1' 0) cG' *)
fprintf ppf "@ @[| %a => %a@]@ "
(fmt_ppr_pat_obj cD1' cG' 0) pat
(* NOTE: Technically: cD |- cG ctx and
* cD1' |- mcomp (MShift n) t <= cD where n = |cD1|
* -bp
*)
(fmt_ppr_cmp_exp_chk cD1' cG_ext 1) e
else
fprintf ppf "@ @[<v2>| @[<v0>%a ; %a@[ |- %a : %a @] => @]@ @[<2>@ %a@]@]@ "
(fmt_ppr_cmp_branch_prefix 0) cD1'
(fmt_ppr_cmp_gctx cD1' 0) cG'
(fmt_ppr_pat_obj cD1' cG' 0) pat
(* this point is where the " : " is in the string above *)
(fmt_ppr_refinement cD1' cD 2) t
(* NOTE: Technically: cD |- cG ctx and
* cD1' |- mcomp (MShift n) t <= cD where n = |cD1|
* -bp
*)
(fmt_ppr_cmp_exp_chk cD1' cG_ext 1) e

(* cD |- t : cD' *)

Expand Down

0 comments on commit 66c66c4

Please sign in to comment.