Commit e6c4bf29 authored by Heiko Becker's avatar Heiko Becker

Small scripts to count lines for coq and hol light dev, cleanup

parent 53709bdb
#!/bin/bash
arr=()
while IFS= read -r -d $'\0'; do
arr+=("$REPLY")
done < <(find . -path ./attic -prune -o -path ./output -prune -o -path ./Infra -prune -o -name "*.v" -print0)
for file in "${arr[@]}"
do
wc -l $file
done
(*
Daisy output:
[ Info ]
[ Info ] Starting specs preprocessing phase
[ Info ] Finished specs preprocessing phase
[ Info ]
[ Info ]
[ Info ] Starting range-error phase
[ Info ] Machine epsilon 5.9604645E-8
[ Info ] 331.4: [331.4, 331.4], 2.8421709430404007e-14
[ Info ] u: [-100.0, 100.0], 7.105427357601002e-15
[ Info ] (331.4 + u): [231.4, 431.4],6.394884621840902e-14
[ Info ] Finished range-error phase
[ Info ]
[ Info ] Starting info phase
[ Info ] doppler
[ Info ] abs-error: 6.394884621840902e-14, range: [231.4, 431.4],
[ Info ] rel-error: 2.7635629307869066E-16
[ Info ] Finished info phase
[ Info ] time:
[ Info ] info: 8 ms, rangeError: 81 ms, analysis: 14 ms, frontend: 2547 ms,
*)
needs "./AbsoluteError.hl";;
let cst = define `cst:real = (&1657) / (&5)`;;
let cstEps = define
`cstEps:err = realFromNum 28421709430404007 16 14`;;
let u = define `u = 1`;;
let varuEps = define
`varuEps:err = realFromNum 7105427357601002 15 15`;;
let lowerBoundAddUCst = define
`lowerBoundAddUCst = -- (&1157) / (&5)`;;
let upperBoundAddUCst = define
`upperBoundAddUCst = (&2157) / (&5)`;;
let addUCstEps = define
`addUCstEps:err = realFromNum 6394884621840902 15 14`;;
let defaultVal = define
`defaultVal = ((&0,&0),&0)`;;
let absenv = define
`absenv (e:(real)exp) =
if e = Const cst
then ((cst,cst),cstEps)
else
if e = Var u
then ((-- &(100),&100), varuEps)
else
if e = Binop Plus (Const cst) (Var u)
then ((lowerBoundAddUCst,upperBoundAddUCst), addUCstEps)
else defaultVal`;;
let theExp = define
`theExp = Binop Plus (Const cst) (Var u)`;;
let theInvariant = define
`theInvariant (env:num->real) = (IVlo (IntvFromEnv absenv (Var u)) <= env u /\ env u <= IVhi (IntvFromEnv absenv (Var u)))`;;
g `!env vR vF.
theInvariant env /\
eval_exp (&0) env theExp vR /\
eval_exp m_eps env theExp vF ==>
AbsErrExp theExp absenv (ErrFromEnv absenv theExp) /\ abs (vR - vF) <= (ErrFromEnv absenv theExp)`;;
e (intros "!env vR vF;inv_valid eval_real eval_float");;
e (CONJ_TAC);;
e (REWRITE_TAC[theExp; absenv; ErrFromEnv]);;
e (ONCE_REWRITE_TAC [AbsErrExp_CASES]);;
e (REPEAT DISJ2_TAC);;
e (EXISTS_TAC `Plus:binop` THEN EXISTS_TAC `(Const cst):(real)exp` THEN EXISTS_TAC `(Var u):(real)exp`);;
e (CONJ_TAC THEN TRY reflexivity);;
e (COND_CASES_TAC THEN TRY COND_CASES_TAC);;
e (contradiction `Binop Plus (Const cst) (Var u) = Const cst` "exp");;
e (contradiction `Binop Plus (Const cst) (Var u) = Var u` "exp");;
e (REWRITE_TAC[SND]);;
e (REWRITE_TAC[absenv; ErrFromEnv]);;
e (ASM_SIMP_TAC[]);;
e (CONJ_TAC);;
(* NEEDS REAL MACHINE EPSILON, THEN EASY PROOF *)
e (CHEAT_TAC);;
(* SAME HERE *)
e (CHEAT_TAC);;
(* Semantic Validation *)
e (ASM_REWRITE_TAC [absenv; ErrFromEnv; theExp]);;
e (COND_CASES_TAC);;
e (contradiction `Binop Plus (Const cst) (Var u) = Const cst` "exp");;
e (COND_CASES_TAC);;
e (contradiction `Binop Plus (Const cst) (Var u) = Var u` "exp");;
e (REWRITE_TAC [SND; addUCstEps]);;
e (RULE_ASSUM_TAC (ONCE_REWRITE_RULE [theExp]));;
e (RULE_ASSUM_TAC (ONCE_REWRITE_RULE [eval_exp_CASES]));;
e (destruct "eval_real" "varcase| constcase | binopcase");;
e (lcontra "varcase" "exp");;
e (lcontra "constcase" "exp");;
e (destruct "eval_float" "fvarcase | fconstcase| fbinopcase");;
e (lcontra "fvarcase" "exp");;
e (lcontra "fconstcase" "exp");;
e (destruct "binopcase" "@b. @e1. @e2. @v1. @v2. @delta. beq vReq eval_e1 eval_e2 delta_less");;
e (destruct "fbinopcase" "@bf. @fe1. @fe2. @fv1. @fv2. @fdelta. fbeq vFeq eval_fe1 eval_fe2 fdelta_less");;
e (RULE_ASSUM_TAC (ONCE_REWRITE_RULE [injectivity "exp"]));;
e (destruct "beq" "plus_b cst_e1 u_e2");;
e (destruct "fbeq" "plus_fb cst_fe1 u_fe2");;
e (RULE_ASSUM_TAC (ONCE_REWRITE_RULE [perturb]));;
e (SUBGOAL_TAC "delta0" `delta = &0` [ALL_TAC]);;
e (MATCH_MP_TAC abs_leq_0_impl_zero);;
e (ASM_REWRITE_TAC[]);;
e (ASM_REWRITE_TAC[perturb]);;
e (REMOVE_THEN "cst_e1" (fun th -> RULE_ASSUM_TAC (ONCE_REWRITE_RULE [SYM th])));;
e (REMOVE_THEN "u_e2" (fun th -> RULE_ASSUM_TAC (ONCE_REWRITE_RULE [SYM th])));;
e (REMOVE_THEN "cst_fe1" (fun th -> RULE_ASSUM_TAC (ONCE_REWRITE_RULE [SYM th])));;
e (REMOVE_THEN "u_fe2" (fun th -> RULE_ASSUM_TAC (ONCE_REWRITE_RULE [SYM th])));;
e (REMOVE_THEN "delta0" (fun th -> RULE_ASSUM_TAC (ONCE_REWRITE_RULE [th])));;
e (USE_THEN "plus_b" (fun th1 -> USE_THEN "plus_fb" (fun th2 -> REWRITE_TAC[SYM th1; SYM th2])));;
e (REMOVE_THEN "plus_b" (fun th -> RULE_ASSUM_TAC (ONCE_REWRITE_RULE [SYM th])));;
e (REMOVE_THEN "plus_fb" (fun th -> RULE_ASSUM_TAC (ONCE_REWRITE_RULE [SYM th])));;
e (REMOVE_THEN "vReq" (fun th -> ONCE_REWRITE_TAC [th]));;
e (REMOVE_THEN "vFeq" (fun th -> ONCE_REWRITE_TAC [th]));;
e (RULE_ASSUM_TAC (ONCE_REWRITE_RULE [eval_exp_CASES]));;
e (destruct "eval_e1" "varcase| constcase | binopcase");;
e (lcontra "varcase" "exp");;
e (destruct "eval_fe1" "fvarcase | fconstcase| fbinopcase");;
e (lcontra "fvarcase" "exp");;
e (destruct "eval_e2" "varcase2 | constcase2 | binopcase2");;
e (destruct "eval_fe2" "fvarcase2 | fconstcase2 | fbinopcase2");;
e (destruct "constcase" "@n. @delta1. cst_n v1_n delta_0");;
e (destruct "fconstcase" "@nf. @fdelta1. cst_fn v1_fn fdelta_less");;
e (destruct "varcase2" "@v. u_v v2_env");;
e (destruct "fvarcase2" "@vf. u_vf v2f_env");;
e (SUBGOAL_TAC "delta10" `delta1 = &0` [MATCH_MP_TAC abs_leq_0_impl_zero THEN ASM_REWRITE_TAC[]]);;
e (REMOVE_THEN "delta_less" (fun th -> REMOVE_THEN "delta_0" (fun th -> ALL_TAC)));;
e (RULE_ASSUM_TAC (REWRITE_RULE[perturb; injectivity "exp"]));;
e (REMOVE_THEN "delta10" (fun th -> RULE_ASSUM_TAC (ONCE_REWRITE_RULE [th])));;
e (REMOVE_THEN "v2f_env" (fun th -> REWRITE_TAC[th]));;
e (REMOVE_THEN "v2_env" (fun th -> REWRITE_TAC[th]));;
e (REMOVE_THEN "u_vf" (fun th -> REWRITE_TAC[SYM th]));;
e (REMOVE_THEN "u_v" (fun th -> REWRITE_TAC[SYM th]));;
e (REMOVE_THEN "v1_fn" (fun th -> REWRITE_TAC[th]));;
e (REMOVE_THEN "cst_fn" (fun th -> REWRITE_TAC[SYM th]));;
e (REMOVE_THEN "v1_n" (fun th -> REWRITE_TAC[th]));;
e (REMOVE_THEN "cst_n" (fun th -> REWRITE_TAC[SYM th]));;
e (REWRITE_TAC [eval_binop]);;
e (SUBGOAL_TAC "var_correct" `contained (IntvFromEnv absenv (Var u)) (env u )` [ALL_TAC]);;
e (RULE_ASSUM_TAC (ONCE_REWRITE_RULE [theInvariant]));;
e (destruct "inv_valid" "invlo invhi");;
e (ASM_REWRITE_TAC [contained]);;
e (SUBGOAL_TAC "cst_correct" `contained (IntvFromEnv absenv (Const cst)) (cst)` [ALL_TAC]);;
e (ASM_REWRITE_TAC [contained; IntvFromEnv; absenv; IVlo; IVhi; REAL_LE_REFL]);;
(** TODO **)
(* Show env u contained in absenv (Var u)
then Const cst contained in absenv (Const cst)
finally conclude u + cst in absenv (u + cst)
*)
e (lcontra "fconstcase2" "exp");;
e (lcontra "fbinopcase2" "exp");;
e (lcontra "constcase2" "exp");;
e (lcontra "binopcase2" "exp");;
e (lcontra "fbinopcase" "exp");;
e (lcontra "binopcase" "exp");;
let theThm = top_thm();;
#!/bin/bash
arr=()
while IFS= read -r -d $'\0'; do
arr+=("$REPLY")
done < <(find . -path ./attic -prune -o -path ./output -prune -o -path ./Infra -prune -o -name "*.hl" -print0)
for file in "${arr[@]}"
do
wc -l $file
done
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment