diff options
| author | Brian Campbell | 2019-04-15 12:08:28 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-04-15 12:08:28 +0100 |
| commit | 1f421b865a87a161a82550443a0cf39aa2642d9c (patch) | |
| tree | 61cd10e0203c7e613ba280c73360abfecad38277 /src/constant_propagation.ml | |
| parent | 57443173923e87f33713c99dbab9eba7e3db0660 (diff) | |
Basic loop termination measures for Coq
Currently only supports pure termination measures for loops with effects.
The user syntax uses separate termination measure declarations, as in the
previous recursive termination measures, which are rewritten into the
loop AST nodes before type checking (because it would be rather difficult
to calculate the correct environment to type check the separate declaration
in).
Diffstat (limited to 'src/constant_propagation.ml')
| -rw-r--r-- | src/constant_propagation.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/constant_propagation.ml b/src/constant_propagation.ml index 5c99a534..ee5678a8 100644 --- a/src/constant_propagation.ml +++ b/src/constant_propagation.ml @@ -440,11 +440,17 @@ let const_props defs ref_vars = let assigns = isubst_minus_set assigns (assigned_vars e4) in let e4',_ = const_prop_exp (Bindings.remove id (fst substs),snd substs) assigns e4 in re (E_for (id,e1',e2',e3',ord,e4')) assigns - | E_loop (loop,e1,e2) -> + | E_loop (loop,m,e1,e2) -> let assigns = isubst_minus_set assigns (IdSet.union (assigned_vars e1) (assigned_vars e2)) in + let m' = match m with + | Measure_aux (Measure_none,_) -> m + | Measure_aux (Measure_some exp,l) -> + let exp',_ = const_prop_exp substs assigns exp in + Measure_aux (Measure_some exp',l) + in let e1',_ = const_prop_exp substs assigns e1 in let e2',_ = const_prop_exp substs assigns e2 in - re (E_loop (loop,e1',e2')) assigns + re (E_loop (loop,m',e1',e2')) assigns | E_vector es -> let es',assigns = non_det_exp_list es in begin |