examples/HolCheck/envTools.sml

35 fun dest_env ie = let val (test,x,ie2) = dest_cond(body(snd(dest_eq(concl(ONCE_REWRITE_CONV [ENV_UPDATE_def] ie)))))
46 (*given an env ie s.t. ie(bv)=X, return |- ie(bv) = X without simplifying X and without opening up ie (which is a huge nested cond)*)
48 fun eval_env_thm ie ieo bv seth thl =
49     let val (e,(v,x)) = dest_env ie
56 fun eval_env ie ieo bv state seth sel thl =
57     mk_lthm (fn _ => (mk_eq(mk_comb(ieo,bv),get_env_val state bv ie),(fn _ => eval_env_thm ie ieo bv seth thl)))
58             (fn _ => eval_env_thm ie ieo bv seth thl)
62 fun strip_env state ie =
63     if (Term.compare(ie, inst [alpha|->type_of state] empty_env_tm)=EQUAL) then []
64     else let val (ie2,(q,s)) = dest_env ie in (q,s)::(strip_env state ie2) end
66 (* returns the prefix of ie upto and including the last assignment to q *)
67 fun env_prefix state q ie =
68     fst (List.foldl (fn ((q',s),(ie,done)) => if done then (ie,done) else
69                      let val (ie',(_,_)) = dest_env ie in if (Term.compare(q,q')=EQUAL) then (ie,true) else (ie',false) end)
70          (ie,false) (strip_env state ie))
72 (* conversional to access the nth-last map's value in an ie *)
73 fun ENV_FIND_CONV ie 0 = RAND_CONV
74 | ENV_FIND_CONV ie n = RATOR_CONV o RATOR_CONV o RAND_CONV o (ENV_FIND_CONV ie (n-1))
76 (* return theorems for normalised ie and ie', in which the mapping in which ie and ie' are different is moved to the end.
77    ASSERT: ie and ie' are different in only one mapping *semantically*
79            to {} in ie and FP....0 in ie' (and analogously for gfp's)
80    ASSERT: in ie and ie', the map order is the same i.e. nth mapping in both is for the same var *)
81 fun ENV_NORM_CONV seth state ie ie' =
82     if (Term.compare(ie,ie')=EQUAL) then (REFL ie,REFL ie') else
85         val _ = print_term ie val _ = print " enc ie\n"(*DBG*)
86         val _ = print_term ie' val _ = print " enc ie'\n"(*DBG*)
87         val maps = strip_env state ie
88         val maps' = strip_env state ie'
93         val (ie_eqth,_) = List.foldl (fn (eqth,(ie,n)) => (* |- old_ie = old_ie with {}'s replaced by appropriate values to match ie' *)
95                                      then (CONV_RULE(RHS_CONV(ENV_FIND_CONV ie n (ONCE_REWRITE_CONV [GSYM(Option.valOf eqth)]))) ie,n+1)
96                                      else (ie,n)) ((REFL ie),0) eqths
101         val (suffix,_) = List.foldl (fn (((q,s),(q',s')),(l,done)) => (* suffix of (ie2,ie') upto the differing mapping *)
105         val res = if List.length suffix=1 then (ie_eqth,REFL ie') (* diff map already at the end *)
110                         List.foldl (fn ((q',s'),ie) =>
111                                     let val iet = rhs(concl ie)
118                                     in CONV_RULE (RHS_CONV (ONCE_REWRITE_CONV [th])) ie end)
120                 in (mv_map_to_end_CONV (q,s) rest ie_eqth,mv_map_to_end_CONV (q',s') rest' (REFL ie')) end